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
-------------------------------------------------------------------- *)
--------------------------------------------------------------------
Copyright (c) - 2015--2016 - IMDEA Software Institute
Copyright (c) - 2015--2018 - Inria
Copyright (c) - 2016--2018 - Polytechnique
-------------------------------------------------------------------- *)
An axiomatization of real numbers
This file provides a classical axiomatization of real numbers as a
discrete real archimedean field with in particular a theory of floor and
ceil.
realType == type of real numbers
sup A == where A : set R with R : realType, the supremum of A when
it exists, 0 otherwise
inf A := - sup (- A)
The mixin corresponding to realType extends an archiFieldType with two
properties:
- when sup A exists, it is an upper bound of A (lemma sup_upper_bound)
- when sup A exists, there exists an element x in A such that
sup A - eps < x for any 0 < eps (lemma sup_adherent)
Rint == the set of real numbers that can be written as z%:~R, i.e., as an integer Rtoint r == r when r is an integer, 0 otherwise
From mathcomp Require Import all_ssreflect all_algebra.
Require Import mathcomp_extra boolp classical_sets.
Require Import Setoid.
Declare Scope real_scope.
Require Import Setoid.
Declare Scope real_scope.
Set Implicit Arguments.
Import Order.TTheory Order.Syntax GRing.Theory Num.Def Num.Theory.
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 setNK : involutive (fun E ⇒ -%R @` E).
Lemma memNE E x : E x = (-%R @` E) (- x).
Lemma lb_ubN E x : lbound E x ↔ ubound (-%R @` E) (- x).
Lemma ub_lbN E x : ubound E x ↔ lbound (-%R @` E) (- x).
Lemma nonemptyN E : nonempty (-%R @` E) ↔ nonempty E.
Lemma opp_set_eq0 E : (-%R @` E) = set0 ↔ E = set0.
Lemma has_lb_ubN E : has_lbound E ↔ has_ubound (-%R @` E).
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 (@setT R) = set0.
End subr_image.
Section has_bound_lemmas.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.
Lemma has_ubPn {E} : ¬ has_ubound E ↔ (∀ x, exists2 y, E y & x < y).
Lemma has_lbPn E : ¬ has_lbound E ↔ (∀ x, exists2 y, E y & y < x).
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.
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 setNK : involutive (fun E ⇒ -%R @` E).
Lemma memNE E x : E x = (-%R @` E) (- x).
Lemma lb_ubN E x : lbound E x ↔ ubound (-%R @` E) (- x).
Lemma ub_lbN E x : ubound E x ↔ lbound (-%R @` E) (- x).
Lemma nonemptyN E : nonempty (-%R @` E) ↔ nonempty E.
Lemma opp_set_eq0 E : (-%R @` E) = set0 ↔ E = set0.
Lemma has_lb_ubN E : has_lbound E ↔ has_ubound (-%R @` E).
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 (@setT R) = set0.
End subr_image.
Section has_bound_lemmas.
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.
Lemma has_ubPn {E} : ¬ has_ubound E ↔ (∀ x, exists2 y, E y & x < y).
Lemma has_lbPn E : ¬ has_lbound E ↔ (∀ x, exists2 y, E y & y < x).
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.
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.
Local Notation "-` E" := [pred x | - x \in E]
(at level 35, right associativity) : fun_scope.
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.
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.
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.
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.
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.
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 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.
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 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.
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 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.
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.