Library mathcomp.analysis.Rstruct

(* This file is a modification of an eponymous file from the CoqApprox        
 library. The header of the original file is reproduced below. Changes are  
 part of the analysis library and enjoy the same licence as this library.   

This file is part of the CoqApprox formalization of rigorous
polynomial approximation in Coq:
http://tamadi.gforge.inria.fr/CoqApprox/

Copyright (c) 2010-2013, ENS de Lyon and Inria.

This library is governed by the CeCILL-C license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/or redistribute the library under the terms of the CeCILL-C
license as circulated by CEA, CNRS and Inria at the following URL:
http://www.cecill.info/

As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the library's author, the holder of
the economic rights, and the successive licensors have only limited
liability. See the COPYING file for more details.
*)

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.
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) :
  (∃ x : R, P x) → ∃ 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 : ∀ x y, reflect (Rle x y) (x ≤ y)%R.
Lemma RltP : ∀ 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_numArchiDomainType := ArchiDomainType R Rarchimedean_axiom. 
 (* Canonical R_numArchiFieldType := numArchiFieldType of R. *)
 Canonical R_realArchiDomainType := realArchiDomainType of R. *)
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):
(∀ 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.
Require Import reals boolp classical_sets.

Section ssreal_struct_contd.

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

Lemma boundE (E : set R) : bound E = has_ubound E.

Lemma completeness' (E : set R) : has_sup E → {m : R | is_lub E m}.

Definition real_sup (E : set R) : R :=
  if pselect (has_sup E) isn't left hsE then 0 else projT1 (completeness' hsE).

Lemma real_sup_is_lub (E : set R) : has_sup E → is_lub E (real_sup E).

Lemma real_sup_ub (E : set R) : has_sup E → (ubound E) (real_sup E).

Lemma real_sup_out (E : set R) : ¬ has_sup E → real_sup E = 0.

Lemma real_sup_adherent (E : set R) (eps : R) :
  has_sup E → 0 < eps → exists2 e : R, E e & (real_sup E - eps) < e.

Definition real_realMixin : Real.mixin_of _ :=
  RealMixin real_sup_ub real_sup_adherent real_sup_out.
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}.

Definition bigmaxr (r : R) s := \big[Num.max/head r s]_(i <- s) i.

Lemma bigmaxr_nil (x0 : R) : bigmaxr x0 [::] = x0.

Lemma bigmaxr_un (x0 x : R) : bigmaxr x0 [:: x] = x.

Lemma bigmaxrE (r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s).

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).

Lemma bigmaxr_cons (x0 x y : R) lr :
  bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)).

Lemma bigmaxr_ler (x0 : R) s i :
  (i < size s)%N → (nth x0 s i) ≤ (bigmaxr x0 s).

Lemma bigmaxr_addr (x0 : R) lr (x : R) :
  bigmaxr (x0 + x) (map (fun y : R ⇒ y + x) lr) = (bigmaxr x0 lr) + x.

Lemma bigmaxr_mem (x0 : R) lr : (0 < size lr)%N → bigmaxr x0 lr \in lr.

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).

Lemma bigmaxr_index (x0 : R) lr :
  (0 < size lr)%N → (index (bigmaxr x0 lr) lr < size lr)%N.

Lemma bigmaxr_lerP (x0 : R) lr (x : R) :
  (0 < size lr)%N →
  reflect (∀ i, (i < size lr)%N → (nth x0 lr i) ≤ x) ((bigmaxr x0 lr) ≤ x).

Lemma bigmaxr_ltrP (x0 : R) lr (x : R) :
  (0 < size lr)%N →
  reflect (∀ i, (i < size lr)%N → (nth x0 lr i) < x) ((bigmaxr x0 lr) < x).

Lemma bigmaxrP (x0 : R) lr (x : R) :
  (x \in lr ∧ ∀ i, (i < size lr) %N → (nth x0 lr i) ≤ x) → (bigmaxr x0 lr = x).

Lemma bigmaxr_lerif (x0 : R) lr :
  uniq lr → ∀ i, (i < size lr)%N →
     (nth x0 lr i) ≤ (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr).

Definition bmaxrf n (f : {ffun 'I_n.+1 → R}) :=
  bigmaxr (f ord0) (codom f).

Lemma bmaxrf_ler n (f : {ffun 'I_n.+1 → R}) i :
  (f i) ≤ (bmaxrf f).

Lemma bmaxrf_index n (f : {ffun 'I_n.+1 → R}) :
  (index (bmaxrf f) (codom f) < n.+1)%N.

Definition index_bmaxrf n f := Ordinal (@bmaxrf_index n f).

Lemma ordnat i n (ord_i : (i < n)%N) : i = Ordinal ord_i :> nat.

Lemma eq_index_bmaxrf n (f : {ffun 'I_n.+1 → R}) :
  f (index_bmaxrf f) = bmaxrf f.

Lemma bmaxrf_lerif n (f : {ffun 'I_n.+1 → R}) :
  injective f → ∀ i,
     (f i) ≤ (bmaxrf f) ?= iff (i == index_bmaxrf f).

End bigmaxr.

End ssreal_struct_contd.

Require Import signed topology normedtype.

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 ↔
  ∀ 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 ↔
  ∀ 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.