Module mathcomp.analysis.Rstruct

Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
Require Import Rtrigo1 Reals.
From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope R_scope.

Lemma Req_EM_T ( r1 r2 : R) : {r1 = r2} + {r1 <> r2}.

Definition eqr ( r1 r2 : R) : bool :=
  if Req_EM_T r1 r2 is left _ then true else false.

Lemma eqrP : Equality.axiom eqr.

Canonical R_eqMixin := EqMixin eqrP.
Canonical R_eqType := Eval hnf in EqType R R_eqMixin.

Fact inhR : inhabited R.

Definition pickR ( P : pred R) ( n : nat) :=
  let x := epsilon inhR P in if P x then Some x else None.

Fact pickR_some P n x : pickR P n = Some x -> P x.

Fact pickR_ex ( P : pred R) :
  (exists x : R, P x) -> exists n, pickR P n.

Fact pickR_ext ( P Q : pred R) : P =1 Q -> pickR P =1 pickR Q.

Definition R_choiceMixin : choiceMixin R :=
  Choice.Mixin pickR_some pickR_ex pickR_ext.

Canonical R_choiceType := Eval hnf in ChoiceType R R_choiceMixin.

Fact RplusA : associative (Rplus).

Definition R_zmodMixin := ZmodMixin RplusA Rplus_comm Rplus_0_l Rplus_opp_l.

Canonical R_zmodType := Eval hnf in ZmodType R R_zmodMixin.

Fact RmultA : associative (Rmult).

Fact R1_neq_0 : R1 != R0.

Definition R_ringMixin := RingMixin RmultA Rmult_1_l Rmult_1_r
  Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.

Canonical R_ringType := Eval hnf in RingType R R_ringMixin.
Canonical R_comRingType := Eval hnf in ComRingType R Rmult_comm.

Import Monoid.

Canonical Radd_monoid := Law RplusA Rplus_0_l Rplus_0_r.
Canonical Radd_comoid := ComLaw Rplus_comm.

Canonical Rmul_monoid := Law RmultA Rmult_1_l Rmult_1_r.
Canonical Rmul_comoid := ComLaw Rmult_comm.

Canonical Rmul_mul_law := MulLaw Rmult_0_l Rmult_0_r.
Canonical Radd_add_law := AddLaw Rmult_plus_distr_r Rmult_plus_distr_l.

Definition Rinvx r := if (r != 0) then / r else r.

Definition unit_R r := r != 0.

Lemma RmultRinvx : {in unit_R, left_inverse 1 Rinvx Rmult}.

Lemma RinvxRmult : {in unit_R, right_inverse 1 Rinvx Rmult}.

Lemma intro_unit_R x y : y * x = 1 /\ x * y = 1 -> unit_R x.

Lemma Rinvx_out : {in predC unit_R, Rinvx =1 id}.

Definition R_unitRingMixin :=
  UnitRingMixin RmultRinvx RinvxRmult intro_unit_R Rinvx_out.

Canonical R_unitRing :=
  Eval hnf in UnitRingType R R_unitRingMixin.

Canonical R_comUnitRingType :=
  Eval hnf in [comUnitRingType of R].

Lemma R_idomainMixin x y : x * y = 0 -> (x == 0) || (y == 0).

Canonical R_idomainType := Eval hnf in IdomainType R R_idomainMixin.

Lemma R_fieldMixin : GRing.Field.mixin_of [unitRingType of R].

Definition R_fieldIdomainMixin := FieldIdomainMixin R_fieldMixin.

Canonical R_fieldType := FieldType R R_fieldMixin.


Definition Rleb r1 r2 := if Rle_dec r1 r2 is left _ then true else false.
Definition Rltb r1 r2 := Rleb r1 r2 && (r1 != r2).
Definition Rgeb r1 r2 := Rleb r2 r1.
Definition Rgtb r1 r2 := Rltb r2 r1.

Lemma RlebP r1 r2 : reflect (r1 <= r2) (Rleb r1 r2).

Lemma RltbP r1 r2 : reflect (r1 < r2) (Rltb r1 r2).


Section ssreal_struct .

Import GRing.Theory.
Import Num.Theory.
Import Num.Def.

Local Open Scope R_scope.

Lemma Rleb_norm_add x y : Rleb (Rabs (x + y)) (Rabs x + Rabs y).

Lemma addr_Rgtb0 x y : Rltb 0 x -> Rltb 0 y -> Rltb 0 (x + y).

Lemma Rnorm0_eq0 x : Rabs x = 0 -> x = 0.

Lemma Rleb_leVge x y : Rleb 0 x -> Rleb 0 y -> (Rleb x y) || (Rleb y x).

Lemma RnormM : {morph Rabs : x y / x * y}.

Lemma Rleb_def x y : (Rleb x y) = (Rabs (y - x) == y - x).

Lemma Rltb_def x y : (Rltb x y) = (y != x) && (Rleb x y).

Definition R_numMixin := NumMixin Rleb_norm_add addr_Rgtb0 Rnorm0_eq0
                                  Rleb_leVge RnormM Rleb_def Rltb_def.
Canonical R_porderType := POrderType ring_display R R_numMixin.
Canonical R_numDomainType := NumDomainType R R_numMixin.
Canonical R_normedZmodType := NormedZmodType R R R_numMixin.

Lemma RleP : forall x y, reflect (Rle x y) (x <= y)%R.
Lemma RltP : forall x y, reflect (Rlt x y) (x < y)%R.

Canonical R_numFieldType := [numFieldType of R].

Lemma Rreal_axiom ( x : R) : (0 <= x)%R || (x <= 0)%R.

Lemma R_total : totalPOrderMixin R_porderType.

Canonical R_latticeType := LatticeType R R_total.
Canonical R_distrLatticeType := DistrLatticeType R R_total.
Canonical R_orderType := OrderType R R_total.
Canonical R_realDomainType := [realDomainType of R].
Canonical R_realFieldType := [realFieldType of R].

Lemma Rarchimedean_axiom : Num.archimedean_axiom R_numDomainType.

Canonical R_realArchiFieldType := ArchiFieldType R Rarchimedean_axiom.


Lemma continuity_eq f g : f =1 g -> continuity f -> continuity g.

Lemma continuity_sum ( I : finType) F ( P : pred I):
(forall i, P i -> continuity (F i)) ->
continuity (fun x => (\sum_( i | P i) ((F i) x)))%R.

Lemma continuity_exp f n: continuity f -> continuity (fun x => (f x)^+ n)%R.

Lemma Rreal_closed_axiom : Num.real_closed_axiom R_numDomainType.

Canonical R_rcfType := RcfType R Rreal_closed_axiom.

End ssreal_struct.

Local Open Scope ring_scope.
From mathcomp Require Import boolp classical_sets.
Require Import reals.

Section ssreal_struct_contd .
Implicit Type E : set R.

Lemma is_upper_boundE E x : is_upper_bound E x = (ubound E) x.

Lemma boundE E : bound E = has_ubound E.

Lemma Rcondcomplete E : has_sup E -> {m | isLub E m}.

Lemma Rsupremums_neq0 E : has_sup E -> (supremums E !=set0)%classic.

Lemma Rsup_isLub x0 E : has_sup E -> isLub E (supremum x0 E).

Lemma real_sup_adherent x0 E ( eps : R) : (0 < eps) ->
  has_sup E -> exists2 e, E e & (supremum x0 E - eps) < e.

Lemma Rsup_ub x0 E : has_sup E -> (ubound E) (supremum x0 E).

Definition real_realMixin : Real.mixin_of _ :=
  RealMixin (@Rsup_ub (0 : R)) (real_sup_adherent 0).
Canonical real_realType := RealType R real_realMixin.

Implicit Types (x y : R) (m n : nat).





Lemma expR0 : exp (0 : R) = 1.

Lemma expRD x y : exp x * exp y = exp (x + y).

Lemma expRX x n : exp x ^+ n = exp (x *+ n).

Lemma sinD x y : sin (x + y) = sin x * cos y + cos x * sin y.

Lemma cosD x y : cos (x + y) = (cos x * cos y - sin x * sin y).

Lemma RplusE x y : Rplus x y = x + y

Lemma RminusE x y : Rminus x y = x - y

Lemma RmultE x y : Rmult x y = x * y

Lemma RoppE x : Ropp x = - x

Lemma RinvE x : x != 0 -> Rinv x = x^-1.

Lemma RdivE x y : y != 0 -> Rdiv x y = x / y.

Lemma INRE n : INR n = n%:R.

Lemma RsqrtE x : 0 <= x -> sqrt x = Num.sqrt x.

Lemma RpowE x n : pow x n = x ^+ n.

Lemma RmaxE x y : Rmax x y = Num.max x y.

Lemma RminE x y : Rmin x y = Num.min x y.

Section bigmaxr .
Context {R : realDomainType}.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Definition bigmaxr ( r : R) s := \big[Num.max/head r s]_( i <- s) i.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_nil ( x0 : R) : bigmaxr x0 [::] = x0.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_un ( x0 x : R) : bigmaxr x0 [:: x] = x.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxrE ( r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigrmax_dflt ( x y : R) s : Num.max x (\big[Num.max/x]_( j <- y :: s) j) =
  Num.max x (\big[Num.max/y]_( i <- y :: s) i).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_cons ( x0 x y : R) lr :
  bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_ler ( x0 : R) s i :
  (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_addr ( x0 : R) lr ( x : R) :
  bigmaxr (x0 + x) (map (fun y : R => y + x) lr) = (bigmaxr x0 lr) + x.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_mem ( x0 : R) lr : (0 < size lr)%N -> bigmaxr x0 lr \in lr.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_mulr ( A : finType) ( s : seq A) ( k : R) ( x : A -> R) :
  0 <= k -> bigmaxr 0 (map (fun i => k * x i) s) = k * bigmaxr 0 (map x s).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_index ( x0 : R) lr :
  (0 < size lr)%N -> (index (bigmaxr x0 lr) lr < size lr)%N.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_lerP ( x0 : R) lr ( x : R) :
  (0 < size lr)%N ->
  reflect (forall i, (i < size lr)%N -> (nth x0 lr i) <= x) ((bigmaxr x0 lr) <= x).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_ltrP ( x0 : R) lr ( x : R) :
  (0 < size lr)%N ->
  reflect (forall i, (i < size lr)%N -> (nth x0 lr i) < x) ((bigmaxr x0 lr) < x).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxrP ( x0 : R) lr ( x : R) :
  (x \in lr /\ forall i, (i < size lr) %N -> (nth x0 lr i) <= x) -> (bigmaxr x0 lr = x).


#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bigmaxr_lerif ( x0 : R) lr :
  uniq lr -> forall i, (i < size lr)%N ->
     (nth x0 lr i) <= (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Definition bmaxrf n ( f : {ffun 'I_n.+1 -> R}) :=
  bigmaxr (f ord0) (codom f).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bmaxrf_ler n ( f : {ffun 'I_n.+1 -> R}) i :
  (f i) <= (bmaxrf f).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bmaxrf_index n ( f : {ffun 'I_n.+1 -> R}) :
  (index (bmaxrf f) (codom f) < n.+1)%N.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Definition index_bmaxrf n f := Ordinal (@bmaxrf_index n f).

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma ordnat i n ( ord_i : (i < n)%N) : i = Ordinal ord_i :> nat.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma eq_index_bmaxrf n ( f : {ffun 'I_n.+1 -> R}) :
  f (index_bmaxrf f) = bmaxrf f.

#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
Lemma bmaxrf_lerif n ( f : {ffun 'I_n.+1 -> R}) :
  injective f -> forall i,
     (f i) <= (bmaxrf f) ?= iff (i == index_bmaxrf f).

End bigmaxr.

End ssreal_struct_contd.

Require Import signed topology.

Section analysis_struct .

Canonical R_pointedType := [pointedType of R for pointed_of_zmodule R_ringType].
Canonical R_filteredType :=
  [filteredType R of R for filtered_of_normedZmod R_normedZmodType].
Canonical R_topologicalType : topologicalType := TopologicalType R
  (topologyOfEntourageMixin
    (uniformityOfBallMixin
      (@nbhs_ball_normE _ R_normedZmodType)
      (pseudoMetric_of_normedDomain R_normedZmodType))).
Canonical R_uniformType : uniformType :=
  UniformType R
  (uniformityOfBallMixin (@nbhs_ball_normE _ R_normedZmodType)
    (pseudoMetric_of_normedDomain R_normedZmodType)).
Canonical R_pseudoMetricType : pseudoMetricType R_numDomainType :=
  PseudoMetricType R (pseudoMetric_of_normedDomain R_normedZmodType).

Lemma continuity_pt_nbhs ( f : R -> R) x :
  continuity_pt f x <->
  forall eps : {posnum R}, nbhs x (fun u => `|f u - f x| < eps%:num).

Lemma continuity_pt_cvg ( f : R -> R) ( x : R) :
  continuity_pt f x <-> {for x, continuous f}.

Lemma continuity_ptE ( f : R -> R) ( x : R) :
  continuity_pt f x <-> {for x, continuous f}.

Local Open Scope classical_set_scope.

Lemma continuity_pt_cvg' f x :
  continuity_pt f x <-> f @ x^' --> f x.

Lemma continuity_pt_dnbhs f x :
  continuity_pt f x <->
  forall eps, 0 < eps -> x^' (fun u => `|f x - f u| < eps).

Lemma nbhs_pt_comp ( P : R -> Prop) ( f : R -> R) ( x : R) :
  nbhs (f x) P -> continuity_pt f x -> \near x, P (f x).

End analysis_struct.