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.
From HB Require Import structures.

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.

#[hnf] HB.instance Definition _ := hasDecEq.Build R eqrP.

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.

#[hnf]
HB.instance Definition _ := hasChoice.Build R pickR_some pickR_ex pickR_ext.

Fact RplusA : associative (Rplus).

#[hnf]
HB.instance Definition _ := GRing.isZmodule.Build R
  RplusA Rplus_comm Rplus_0_l Rplus_opp_l.

Fact RmultA : associative (Rmult).

Fact R1_neq_0 : R1 != R0.

#[hnf]
HB.instance Definition _ := GRing.Zmodule_isRing.Build R
  RmultA Rmult_1_l Rmult_1_r Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.

#[hnf]
HB.instance Definition _ := GRing.Ring_hasCommutativeMul.Build R Rmult_comm.

Import Monoid.

HB.instance Definition _ := isComLaw.Build R 0 Rplus
  RplusA Rplus_comm Rplus_0_l.

HB.instance Definition _ := isComLaw.Build R 1 Rmult
  RmultA Rmult_comm Rmult_1_l.

HB.instance Definition _ := isMulLaw.Build R 0 Rmult Rmult_0_l Rmult_0_r.
HB.instance Definition _ := isAddLaw.Build R Rmult Rplus
  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}.

#[hnf]
HB.instance Definition _ := GRing.Ring_hasMulInverse.Build R
  RmultRinvx RinvxRmult intro_unit_R Rinvx_out.

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

#[hnf]
HB.instance Definition _ := GRing.ComUnitRing_isIntegral.Build R
  R_idomainMixin.

Lemma R_fieldMixin : GRing.field_axiom R
HB.instance Definition _ := GRing.UnitRing_isField.Build 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).

HB.instance Definition _ := Num.IntegralDomain_isNumRing.Build R
  Rleb_norm_add addr_Rgtb0 Rnorm0_eq0 Rleb_leVge RnormM Rleb_def Rltb_def.

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

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

Lemma R_total : total (<=%O : rel R).

HB.instance Definition _ := Order.POrder_isTotal.Build _ R R_total.

Lemma Rarchimedean_axiom :
  Num.archimedean_axiom [the numDomainType of R : Type].

HB.instance Definition _ := Num.RealField_isArchimedean.Build 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 [the numDomainType of R : Type].

HB.instance Definition _ := Num.RealField_isClosed.Build 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).

HB.instance Definition _ := ArchimedeanField_isReal.Build R
  (@Rsup_ub (0 : R)) (real_sup_adherent 0).

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.

HB.instance Definition _ := PseudoMetric.copy R R^o.

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.