Library mathcomp.analysis.reals

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              
 -------------------------------------------------------------------- 
 Copyright (c) - 2015--2016 - IMDEA Software Institute                
 Copyright (c) - 2015--2018 - Inria                                   
 Copyright (c) - 2016--2018 - Polytechnique                           
 -------------------------------------------------------------------- *)

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.

Require Import Setoid.

Declare Scope real_scope.

Set Implicit Arguments.

Import Order.TTheory Order.Syntax GRing.Theory Num.Def Num.Theory.

Delimit Scope real_scope with real.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section subr_image.
Variable R : numDomainType.
Implicit Types (E : set R) (x : R).

Lemma has_ub_lbN E : has_ubound E ↔ has_lbound (-%R @` E).

Lemma has_lbound0 : has_lbound (@set0 R).

Lemma has_ubound0 : has_ubound (@set0 R).

Lemma ubound0 : ubound (@set0 R) = setT.

Lemma lboundT : lbound [set: R] = set0.

End subr_image.

Section has_bound_lemmas.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma has_ub_image_norm E : has_ubound (normr @` E) → has_ubound E.

Lemma has_inf_supN E : has_sup (-%R @` E) ↔ has_inf E.

Lemma has_supPn {E} : E !=set0 →
  ¬ has_sup E ↔ (∀ x, exists2 y, E y & x < y).

End has_bound_lemmas.

Module Real.
Section Mixin.

Variable (R : archiFieldType).

Record mixin_of : Type := Mixin {
   _ :
    ∀ E : set (Num.ArchimedeanField.sort R),
      has_sup E → ubound E (supremum 0 E) ;
   _ :
    ∀ (E : set (Num.ArchimedeanField.sort R)) (eps : R), 0 < eps →
      has_sup E → exists2 e : R, E e & (supremum 0 E - eps) < e ;
}.

End Mixin.

Definition EtaMixin R sup_upper_bound sup_adherent :=
  let _ := @Mixin R sup_upper_bound sup_adherent in
  @Mixin (Num.ArchimedeanField.Pack (Num.ArchimedeanField.class R))
         sup_upper_bound sup_adherent.
Section ClassDef.

Record class_of (R : Type) : Type := Class {
  base : Num.ArchimedeanField.class_of R;
  mixin_rcf : Num.real_closed_axiom (Num.NumDomain.Pack base);
  (* TODO: ajouter une structure de pseudoMetricNormedDomain *)
  mixin : mixin_of (Num.ArchimedeanField.Pack base)
}.


Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Variables (T : Type) (cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition rcf_axiom {R} (cR : Num.RealClosedField.class_of R) :
   Num.real_closed_axiom (Num.NumDomain.Pack cR) :=
  match cR with Num.RealClosedField.Class _ ax ⇒ ax end.
Coercion rcf_axiom : Num.RealClosedField.class_of >-> Num.real_closed_axiom.

Definition pack b0 (m0 : mixin_of (@Num.ArchimedeanField.Pack T b0)) :=
  fun bT b & phant_id (Num.ArchimedeanField.class bT) b ⇒
  fun (bTr : rcfType) (br : Num.RealClosedField.class_of bTr) &
      phant_id (Num.RealClosedField.class bTr) br ⇒
  fun cra & phant_id (@rcf_axiom bTr br) cra ⇒
  fun m & phant_id m0 m ⇒ Pack (@Class T b cra m) T.

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition porderType := @Order.POrder.Pack ring_display cT xclass.
Definition latticeType := @Order.Lattice.Pack ring_display cT xclass.
Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass.
Definition orderType := @Order.Total.Pack ring_display cT xclass.
Definition zmodType := @GRing.Zmodule.Pack cT xclass.
Definition ringType := @GRing.Ring.Pack cT xclass.
Definition comRingType := @GRing.ComRing.Pack cT xclass.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
Definition numDomainType := @Num.NumDomain.Pack cT xclass.
Definition normedZmodType := NormedZmodType numDomainType cT xclass.
Definition fieldType := @GRing.Field.Pack cT xclass.
Definition realDomainType := @Num.RealDomain.Pack cT xclass.
Definition numFieldType := @Num.NumField.Pack cT xclass.
Definition realFieldType := @Num.RealField.Pack cT xclass.
Definition archimedeanFieldType := @Num.ArchimedeanField.Pack cT xclass.
Definition rcfType := @Num.RealClosedField.Pack cT xclass.
Definition join_rcfType := @Num.RealClosedField.Pack archimedeanFieldType xclass.

End ClassDef.

Module Exports.
Coercion base : class_of >-> Num.ArchimedeanField.class_of.
Coercion base_rcf : class_of >-> Num.RealClosedField.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion latticeType : type >-> Order.Lattice.type.
Canonical latticeType.
Coercion distrLatticeType : type >-> Order.DistrLattice.type.
Canonical distrLatticeType.
Coercion orderType : type >-> Order.Total.type.
Canonical orderType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> Num.NumDomain.type.
Canonical numDomainType.
Coercion normedZmodType : type >-> Num.NormedZmodule.type.
Canonical normedZmodType.
Coercion realDomainType : type >-> Num.RealDomain.type.
Canonical realDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> Num.NumField.type.
Canonical numFieldType.
Coercion realFieldType : type >-> Num.RealField.type.
Canonical realFieldType.
Coercion archimedeanFieldType : type >-> Num.ArchimedeanField.type.
Canonical archimedeanFieldType.
Coercion rcfType : type >-> Num.RealClosedField.type.
Canonical rcfType.
Canonical join_rcfType.

Notation realType := type.
Notation RealType T m := (@pack T _ m _ _ id _ _ id _ id _ id).
Notation RealMixin := EtaMixin.
Notation "[ 'realType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'realType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'realType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'realType' 'of' T ]") : form_scope.

End Exports.
End Real.

Export Real.Exports.

Definition sup {R : realType} := @supremum _ R 0.

Definition inf {R : realType} (E : set R) := - sup (-%R @` E).

Lemma sup_upper_bound {R : realType} (E : set R):
  has_sup E → ubound E (sup E).

Lemma sup_adherent {R : realType} (E : set R) (eps : R) : 0 < eps →
  has_sup E → exists2 e : R, E e & (sup E - eps) < e.

Section IsInt.
Context {R : realFieldType}.

Definition Rint := [qualify a x : R | `[< ∃ z, x == z%:~R >]].
Fact Rint_key : pred_key Rint.
Canonical Rint_keyed := KeyedQualifier Rint_key.

Lemma Rint_def x : (x \is a Rint) = (`[< ∃ z, x == z%:~R >]).

Lemma RintP x : reflect (∃ z, x = z%:~R) (x \in Rint).

Lemma RintC z : z%:~R \is a Rint.

Lemma Rint0 : 0 \is a Rint.

Lemma Rint1 : 1 \is a Rint.

Hint Resolve Rint0 Rint1 RintC : core.

Lemma Rint_subring_closed : subring_closed Rint.

Canonical Rint_opprPred := OpprPred Rint_subring_closed.
Canonical Rint_addrPred := AddrPred Rint_subring_closed.
Canonical Rint_mulrPred := MulrPred Rint_subring_closed.
Canonical Rint_zmodPred := ZmodPred Rint_subring_closed.
Canonical Rint_semiringPred := SemiringPred Rint_subring_closed.
Canonical Rint_smulrPred := SmulrPred Rint_subring_closed.
Canonical Rint_subringPred := SubringPred Rint_subring_closed.

Lemma Rint_ler_addr1 (x y : R) : x \is a Rint → y \is a Rint →
  (x + 1 ≤ y) = (x < y).

Lemma Rint_ltr_addr1 (x y : R) : x \is a Rint → y \is a Rint →
  (x < y + 1) = (x ≤ y).

End IsInt.

Section ToInt.
Context {R : realType}.

Implicit Types x y : R.

Definition Rtoint (x : R) : int :=
  if insub x : {? x | x \is a Rint} is Some Px then
    xchoose (asboolP _ (tagged Px))
  else 0.

Lemma RtointK (x : R): x \is a Rint → (Rtoint x)%:~R = x.

Lemma Rtointz (z : int): Rtoint z%:~R = z.

Lemma Rtointn (n : nat): Rtoint n%:R = n%:~R.

Lemma inj_Rtoint : {in Rint &, injective Rtoint}.

Lemma RtointN x : x \is a Rint → Rtoint (- x) = - Rtoint x.

End ToInt.

Section RealDerivedOps.
Variable R : realType.

Implicit Types x y : R.
Definition floor_set x := [set y : R | (y \is a Rint) && (y ≤ x)].

Definition Rfloor x : R := sup (floor_set x).

Definition floor x : int := Rtoint (Rfloor x).

Definition range1 (x : R) := [set y | x ≤ y < x + 1].

Definition Rceil x := - Rfloor (- x).

Definition ceil x := - floor (- x).

End RealDerivedOps.

Section RealLemmas.

Variables (R : realType).

Implicit Types E : set R.
Implicit Types x : R.

Lemma sup_out E : ¬ has_sup E → sup E = 0.

Lemma sup0 : sup (@set0 R) = 0.

Lemma sup1 x : sup [set x] = x.

Lemma sup_ub {E} : has_ubound E → ubound E (sup E).

Lemma sup_ub_strict E : has_ubound E →
  ¬ E (sup E) → E `<=` [set r | r < sup E].

Lemma sup_total {E} x : has_sup E → down E x ∨ sup E ≤ x.

Lemma sup_le_ub {E} x : E !=set0 → (ubound E) x → sup E ≤ x.

Lemma sup_setU (A B : set R) : has_sup B →
  (∀ a b, A a → B b → a ≤ b) → sup (A `|` B) = sup B.

Lemma sup_gt (S : set R) (x : R) : S !=set0 →
  (x < sup S → exists2 y, S y & x < y)%R.

End RealLemmas.

Section sup_sum.
Context {R : realType}.

Lemma sup_sumE (A B : set R) :
  has_sup A → has_sup B → sup [set x + y | x in A & y in B] = sup A + sup B.

Lemma inf_sumE (A B : set R) :
  has_inf A → has_inf B → inf [set x + y | x in A & y in B] = inf A + inf B.

End sup_sum.

Section InfTheory.

Variables (R : realType).

Implicit Types E : set R.
Implicit Types x : R.

Lemma inf_lower_bound E : has_inf E → lbound E (inf E).

Lemma inf_adherent E (eps : R) : 0 < eps →
  has_inf E → exists2 e, E e & e < inf E + eps.

Lemma inf_out E : ¬ has_inf E → inf E = 0.

Lemma inf0 : inf (@set0 R) = 0.

Lemma inf1 x : inf [set x] = x.

Lemma inf_lb E : has_lbound E → lbound E (inf E).

Lemma inf_lb_strict E : has_lbound E →
  ¬ E (inf E) → E `<=` [set r | inf E < r].

Lemma lb_le_inf E x : nonempty E → (lbound E) x → x ≤ inf E.

Lemma has_infPn E : nonempty E →
  ¬ has_inf E ↔ (∀ x, exists2 y, E y & y < x).

Lemma inf_setU (A B : set R) : has_inf A →
  (∀ a b, A a → B b → a ≤ b) → inf (A `|` B) = inf A.

Lemma inf_lt (S : set R) (x : R) : S !=set0 →
  (inf S < x → exists2 y, S y & y < x)%R.

End InfTheory.

Section FloorTheory.
Variable R : realType.

Implicit Types x y : R.

Lemma has_sup_floor_set x : has_sup (floor_set x).

Lemma sup_in_floor_set x : (floor_set x) (sup (floor_set x)).

Lemma isint_Rfloor x : Rfloor x \is a Rint.

Lemma RfloorE x : Rfloor x = (floor x)%:~R.

Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.

Lemma Rfloor_le x : Rfloor x ≤ x.

Lemma floor_le x : (floor x)%:~R ≤ x.

Lemma lt_succ_Rfloor x : x < Rfloor x + 1.

Lemma range1z_inj x (m1 m2 : int) :
  (range1 m1%:~R) x → (range1 m2%:~R) x → m1 = m2.

Lemma range1rr x : (range1 x) x.

Lemma range1zP (m : int) x : Rfloor x = m%:~R ↔ (range1 m%:~R) x.

Lemma Rfloor_natz (z : int) : Rfloor z%:~R = z%:~R :> R.

Lemma Rfloor0 : Rfloor 0 = 0 :> R.

Lemma Rfloor1 : Rfloor 1 = 1 :> R.

Lemma le_Rfloor : {homo (@Rfloor R) : x y / x ≤ y}.

Lemma Rfloor_ge_int x (n : int) : (n%:~R ≤ x)= (n%:~R ≤ Rfloor x).

Lemma Rfloor_lt_int x (z : int) : (x < z%:~R) = (Rfloor x < z%:~R).

Lemma Rfloor_le0 x : x ≤ 0 → Rfloor x ≤ 0.

Lemma Rfloor_lt0 x : x < 0 → Rfloor x < 0.

Lemma floor_natz n : floor (n%:R : R) = n%:~R :> int.

Lemma floor0 : floor (0 : R) = 0.

Lemma floor1 : floor (1 : R) = 1.

Lemma floor_ge0 x : (0 ≤ floor x) = (0 ≤ x).

Lemma floor_le0 x : x ≤ 0 → floor x ≤ 0.

Lemma floor_lt0 x : x < 0 → floor x < 0.

Lemma le_floor : {homo @floor R : x y / x ≤ y}.

Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x ≥ 1).

Lemma lt_succ_floor x : x < (floor x)%:~R + 1.

Lemma floor_lt_int x (z : int) : (x < z%:~R) = (floor x < z).

Lemma floor_ge_int x (z : int) : (z%:~R ≤ x) = (z ≤ floor x).

Lemma ltr_add_invr (y x : R) : y < x → ∃ k, y + k.+1%:R^-1 < x.

End FloorTheory.

Section CeilTheory.
Variable R : realType.

Implicit Types x y : R.

Lemma isint_Rceil x : Rceil x \is a Rint.

Lemma Rceil0 : Rceil 0 = 0 :> R.

Lemma Rceil_ge x : x ≤ Rceil x.

Lemma le_Rceil : {homo (@Rceil R) : x y / x ≤ y}.

Lemma Rceil_ge0 x : 0 ≤ x → 0 ≤ Rceil x.

Lemma RceilE x : Rceil x = (ceil x)%:~R.

Lemma ceil_ge x : x ≤ (ceil x)%:~R.

Lemma ceil_ge0 x : 0 ≤ x → 0 ≤ ceil x.

Lemma ceil_gt0 x : 0 < x → 0 < ceil x.

Lemma ceil_le0 x : x ≤ 0 → ceil x ≤ 0.

Lemma le_ceil : {homo @ceil R : x y / x ≤ y}.

Lemma ceil_ge_int x (z : int) : (x ≤ z%:~R) = (ceil x ≤ z).

Lemma ceil_lt_int x (z : int) : (z%:~R < x) = (z < ceil x).

End CeilTheory.

Section Sup.
Context {R : realType}.

Lemma le_down (S : set R) : S `<=` down S.

Lemma downK (S : set R) : down (down S) = down S.

Lemma has_sup_down (S : set R) : has_sup (down S) ↔ has_sup S.

Lemma le_sup (S1 S2 : set R) :
  S1 `<=` down S2 → nonempty S1 → has_sup S2
    → sup S1 ≤ sup S2.

Lemma sup_down (S : set R) : sup (down S) = sup S.

Lemma lt_sup_imfset {T : Type} (F : T → R) l :
  has_sup [set y | ∃ x, y = F x] →
  l < sup [set y | ∃ x, y = F x] →
  exists2 x, l < F x & F x ≤ sup [set y | ∃ x, y = F x].

Lemma lt_inf_imfset {T : Type} (F : T → R) l :
  has_inf [set y | ∃ x, y = F x] →
  inf [set y | ∃ x, y = F x] < l →
  exists2 x, F x < l & inf [set y | ∃ x, y = F x] ≤ F x.

End Sup.

Lemma int_lbound_has_minimum (B : set int) i : B !=set0 → lbound B i →
  ∃ j, B j ∧ ∀ k, B k → j ≤ k.

Section rat_in_itvoo.

Let bound_div (R : archiFieldType) (x y : R) : nat :=
  if y < 0 then 0%N else Num.bound (y / x).

Let archi_bound_divP (R : archiFieldType) (x y : R) :
  0 < x → y < x *+ bound_div x y.

Lemma rat_in_itvoo (R : realType) (x y : R) :
  x < y → ∃ q, ratr q \in `]x, y[.

End rat_in_itvoo.