express sup with supremum

- complete documentation of `classical_sets.v` - documentation of `reals.v` - proof simplications in `reals.v` + `sup_out`, `sup0`, `sup1` now proved as consequences of the definition of `sup` using `supremum` - minor generalizations
math-comp · Jun 8, 2022 · 4cc17d8 · 4cc17d8
1 parent a649cb4
commit 4cc17d8
Show file tree

Hide file tree

Showing 10 changed files with 223 additions and 146 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -33,17 +33,45 @@
   + lemma `floor_natz`
 - in file `topology.v`:
   + definition `frechet_filter`, instances `frechet_properfilter`, and `frechet_properfilter_nat`
+- in `Rstruct.v`:
+  + lemmas `Rsupremums_neq0`, `Rsup_isLub`, `Rsup_ub`
+- in `classical_sets.v`:
+  + lemma `supremum_out`
+  + definition `isLub`
+  + lemma `supremum1`
+- in `reals.v`:
+  + lemma `opp_set_eq0`, `ubound0`, `lboundT`
 
 ### Changed
 
 - in `topology.v`:
   + generalize `cluster_cvgE`, `fam_cvgE`, `ptws_cvg_compact_family`
   + rewrite `equicontinuous` and `pointwise_precompact` to use index 
+- in `Rstruct.v`:
+  + statement of lemma `completeness'`, renamed to `Rcondcomplete`
+  + statement of lemma `real_sup_adherent`
+- in `ereal.v`:
+  + statements of lemmas `ub_ereal_sup_adherent`, `lb_ereal_inf_adherent`
+- in `reals.v`:
+  + definition `sup`
+  + statements of lemmas `sup_adherent`, `inf_adherent`
 
 ### Renamed
 
 ### Removed
 
+- `has_sup1`, `has_inf1` moved from `reals.v` to `classical_sets.v`
+- in `reals.v`:
+  + type generalization of `has_supPn`
+- in `classical_sets.v`:
+  + `supremums_set1` -> `supremums1`
+  + `infimums_set1` -> `infimums1`
+- in `Rstruct.v`:
+  + definition `real_sup`
+  + lemma `real_sup_is_lub`, `real_sup_ub`, `real_sup_out`
+- in `reals.v`:
+  + field `sup` from `mixin_of` in module `Real`
+
 ### Infrastructure
 
 ### Misc
diff --git a/theories/Rstruct.v b/theories/Rstruct.v
@@ -375,50 +375,58 @@ Local Open Scope ring_scope.
 Require Import reals boolp classical_sets.
 
 Section ssreal_struct_contd.
+Implicit Type E : set R.
 
-Lemma is_upper_boundE (E : set R) x : is_upper_bound E x = ((ubound E) x).
+Lemma is_upper_boundE E x : is_upper_bound E x = (ubound E) x.
 Proof.
 rewrite propeqE; split; [move=> h|move=> /ubP h y Ey; exact/RleP/h].
 by apply/ubP => y Ey; apply/RleP/h.
 Qed.
 
-Lemma boundE (E : set R) : bound E = has_ubound E.
+Lemma boundE E : bound E = has_ubound E.
 Proof. by apply/eq_exists=> x; rewrite is_upper_boundE. Qed.
 
-Lemma completeness' (E : set R) : has_sup E -> {m : R | is_lub E m}.
-Proof. by move=> [eE bE]; rewrite -boundE in bE; apply: completeness. Qed.
-
-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 Rcondcomplete E : has_sup E -> {m | isLub E m}.
 Proof.
-by move=> hsE; rewrite /real_sup; case: pselect=> // ?; case: completeness'.
+move=> [E0 uE]; have := completeness E; rewrite boundE => /(_ uE E0)[x [E1 E2]].
+exists x; split; first by rewrite -is_upper_boundE; apply: E1.
+by move=> y; rewrite -is_upper_boundE => /E2/RleP.
 Qed.
 
-Lemma real_sup_ub (E : set R) : has_sup E -> (ubound E) (real_sup E).
-Proof. by move=> /real_sup_is_lub []; rewrite is_upper_boundE. Qed.
+Lemma Rsupremums_neq0 E : has_sup E -> (supremums E !=set0)%classic.
+Proof. by move=> /Rcondcomplete[x [? ?]]; exists x. Qed.
 
-Lemma real_sup_out (E : set R) : ~ has_sup E -> real_sup E = 0.
-Proof. by move=> nosup; rewrite /real_sup; case: pselect. Qed.
+Lemma Rsup_isLub x0 E : has_sup E -> isLub E (supremum x0 E).
+Proof.
+have [-> [/set0P]|E0 hsE] := eqVneq E set0; first by rewrite eqxx.
+have [s [Es sE]] := Rcondcomplete hsE.
+split => x Ex; first by apply/ge_supremum_Nmem=> //; exact: Rsupremums_neq0.
+rewrite /supremum (negbTE E0); case: xgetP => /=.
+  by move=> _ -> [_ EsE]; apply/EsE.
+by have [y Ey /(_ y)] := Rsupremums_neq0 hsE.
+Qed.
 
 (* :TODO: rewrite like this using (a fork of?) Coquelicot *)
 (* Lemma real_sup_adherent (E : pred R) : real_sup E \in closure E. *)
-Lemma real_sup_adherent (E : set R) (eps : R) :
-  has_sup E -> 0 < eps -> exists2 e : R, E e & (real_sup E - eps) < e.
+Lemma real_sup_adherent x0 E (eps : R) : (0 < eps) ->
+  has_sup E -> exists2 e, E e & (supremum x0 E - eps) < e.
 Proof.
-move=> supE eps_gt0; set m := _ - eps; apply: contrapT=> mNsmall.
-have: (ubound E) m.
+move=> eps_gt0 supE; set m := _ - eps; apply: contrapT=> mNsmall.
+have : (ubound E) m.
   apply/ubP => y Ey.
-  have /negP := mNsmall (ex_intro2 _ _ y Ey _).
-  by rewrite -leNgt.
-have [_ /(_ m)] := real_sup_is_lub supE.
-rewrite is_upper_boundE => m_big /m_big /RleP.
+  by have /negP := mNsmall (ex_intro2 _ _ y Ey _); rewrite -leNgt.
+have [_ /(_ m)] := Rsup_isLub x0 supE.
+move => m_big /m_big.
 by rewrite -subr_ge0 addrC addKr oppr_ge0 leNgt eps_gt0.
 Qed.
 
+Lemma Rsup_ub x0 E : has_sup E -> (ubound E) (supremum x0 E).
+Proof.
+by move=> supE x Ex; apply/ge_supremum_Nmem => //; exact: Rsupremums_neq0.
+Qed.
+
 Definition real_realMixin : Real.mixin_of _ :=
-  RealMixin real_sup_ub real_sup_adherent real_sup_out.
+  RealMixin (@Rsup_ub (0 : R)) (real_sup_adherent 0).
 Canonical real_realType := RealType R real_realMixin.
 
 Implicit Types (x y : R) (m n : nat).

diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
@@ -180,7 +180,7 @@ case: (pselect (has_sup E)); last first.
   by apply/(lt_le_trans lt_MuK)/mono_u.
 move=> supE; exists (sup E)%:E => //; first exact: ltNye.
 elim/nbh_finW=>e /= gt0_e.
-case: (sup_adherent supE gt0_e)=> x [K ->] lt_uK.
+case: (sup_adherent gt0_e supE)=> x [K ->] lt_uK.
 exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0.
   by move/ubP: (sup_upper_bound supE); apply; exists n.
 rewrite ltr_subl_addr addrC -ltr_subl_addr.
@@ -467,7 +467,7 @@ apply/eqP; case: (x =P _) => // /eqP /lt_total /orP[]; last first.
   by apply/ler_sum=> /= i _; apply/ler_norm.
 move=> lt_xS; pose e := psum S - x.
   have ge0_e: 0 < e by rewrite subr_gt0.
-case: (sup_adherent (summable_sup smS) ge0_e) => y.
+case: (sup_adherent ge0_e (summable_sup smS)) => y.
 case=> /= J ->; rewrite /e /psum (asboolT smS).
 rewrite opprB addrCA subrr addr0 => lt_xSJ.
 pose k := \max_(j : J) (val j); have lt_x_uSk: x < u k.+1.

diff --git a/theories/classical_sets.v b/theories/classical_sets.v
@@ -119,8 +119,22 @@ Require Import mathcomp_extra boolp.
 (*                pblock D F x := F (pblock_index D F x)                      *)
 (*                                                                            *)
 (* * Upper and lower bounds:                                                  *)
-(*              ubound, lbound == upper bound and lower bound sets            *)
-(*               supremum x0 E == supremum of E or x0 if E is empty           *)
+(*              ubound A == the set of upper bounds of the set A              *)
+(*              lbound A == the set of lower bounds of the set A              *)
+(*   Predicates to express existence conditions of supremum and infimum of    *)
+(*   sets of real numbers:                                                    *)
+(*          has_ubound A := ubound A != set0                                  *)
+(*             has_sup A := A != set0 /\ has_ubound A                         *)
+(*          has_lbound A := lbound A != set0                                  *)
+(*             has_inf A := A != set0 /\ has_lbound A                         *)
+(*                                                                            *)
+(*             isLub A m := m is a least upper bound of the set A             *)
+(*           supremums A := set of supremums of the set A                     *)
+(*         supremum x0 A == supremum of A or x0 if A is empty                 *)
+(*            infimums A := set of infimums of the set A                      *)
+(*          infimum x0 A == infimum of A or x0 if A is empty                  *)
+(*                                                                            *)
+(*               F `#` G := the classes of sets F and G intersect             *)
 (*                                                                            *)
 (* * sections:                                                                *)
 (*           xsection A x == with A : set (T1 * T2) and x : T1 is the         *)
@@ -2575,10 +2589,10 @@ Qed.
 Section UpperLowerTheory.
 Import Order.TTheory.
 Variables (d : unit) (T : porderType d).
-Implicit Types A : set T.
+Implicit Types (A : set T) (x y z : T).
 
-Definition ubound A : set T := [set z | forall y, A y -> (y <= z)%O].
-Definition lbound A : set T := [set z | forall y, A y -> (z <= y)%O].
+Definition ubound A : set T := [set y | forall x, A x -> (x <= y)%O].
+Definition lbound A : set T := [set y | forall x, A x -> (y <= x)%O].
 
 Lemma ubP A x : (forall y, A y -> (y <= x)%O) <-> ubound A x.
 Proof. by []. Qed.
@@ -2614,33 +2628,40 @@ Proof. by move=> Ey; apply. Qed.
 (* i.e. down A := { x | exists y, y \in A /\ x <= y} *)
 Definition down A : set T := [set x | exists y, A y /\ (x <= y)%O].
 
-(* Real set supremum and infimum existence condition. *)
 Definition has_ubound A := ubound A !=set0.
 Definition has_sup A := A !=set0 /\ has_ubound A.
 Definition has_lbound A := lbound A !=set0.
 Definition has_inf A := A !=set0 /\ has_lbound A.
 
+Lemma has_ub_set1 x : has_ubound [set x].
+Proof. by exists x; rewrite ub_set1. Qed.
+
 Lemma has_inf0 : ~ has_inf (@set0 T).
 Proof. by rewrite /has_inf not_andP; left; apply/set0P/negP/negPn. Qed.
 
 Lemma has_sup0 : ~ has_sup (@set0 T).
 Proof. by rewrite /has_sup not_andP; left; apply/set0P/negP/negPn. Qed.
 
+Lemma has_sup1 x : has_sup [set x].
+Proof. by split; [exists x | exists x => y ->]. Qed.
+
+Lemma has_inf1 x : has_inf [set x].
+Proof. by split; [exists x | exists x => y ->]. Qed.
+
 Lemma subset_has_lbound A B : A `<=` B -> has_lbound B -> has_lbound A.
 Proof. by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
 
 Lemma subset_has_ubound A B : A `<=` B -> has_ubound B -> has_ubound A.
 Proof. by move=> AB [l Bl]; exists l => a Aa; apply/Bl/AB. Qed.
 
-Lemma has_ub_set1 x : has_ubound [set x].
-Proof. by exists x; rewrite ub_set1. Qed.
-
 Lemma downP A x : (exists2 y, A y & (x <= y)%O) <-> down A x.
 Proof. by split => [[y Ay xy]|[y [Ay xy]]]; [exists y| exists y]. Qed.
 
+Definition isLub A m := ubound A m /\ forall b, ubound A b -> (m <= b)%O.
+
 Definition supremums A := ubound A `&` lbound (ubound A).
 
-Lemma supremums_set1 x : supremums [set x] = [set x].
+Lemma supremums1 x : supremums [set x] = [set x].
 Proof.
 rewrite /supremums predeqE => y; split => [[]|->{y}]; last first.
   by split; [rewrite ub_set1|exact: lb_ub_refl].
@@ -2649,19 +2670,32 @@ Qed.
 
 Lemma is_subset1_supremums A : is_subset1 (supremums A).
 Proof.
-move=> x y [Ex xE] [Ey yE]; apply/eqP.
-by rewrite eq_le (ub_lb_ub Ex yE) (ub_lb_ub Ey xE).
+move=> x y [Ax xA] [Ay yA]; apply/eqP.
+by rewrite eq_le (ub_lb_ub Ax yA) (ub_lb_ub Ay xA).
 Qed.
 
-Definition supremum (x0 : T) A :=
-  if A == set0 then x0 else xget x0 (supremums A).
+Definition supremum x0 A := if A == set0 then x0 else xget x0 (supremums A).
 
-Definition infimums A := lbound A `&` ubound (lbound A).
+Lemma supremum_out x0 A : ~ has_sup A -> supremum x0 A = x0.
+Proof.
+move=> hsA; rewrite /supremum; case: ifPn => // /set0P[/= x Ax].
+case: xgetP => //= _ -> [uA _]; exfalso.
+by apply: hsA; split; [exists x|exists (xget x0 (supremums A))].
+Qed.
 
-Definition infimum (x0 : T) A :=
-  if A == set0 then x0 else xget x0 (infimums A).
+Lemma supremum0 x0 : supremum x0 set0 = x0.
+Proof. by rewrite /supremum eqxx. Qed.
 
-Lemma infimums_set1 x : infimums [set x] = [set x].
+Lemma supremum1 x0 x : supremum x0 [set x] = x.
+Proof.
+rewrite /supremum ifF; last first.
+  by apply/eqP; rewrite predeqE => /(_ x)[+ _]; apply.
+by rewrite supremums1; case: xgetP => // /(_ x) /(_ erefl).
+Qed.
+
+Definition infimums A := lbound A `&` ubound (lbound A).
+
+Lemma infimums1 x : infimums [set x] = [set x].
 Proof.
 rewrite /infimums predeqE => y; split => [[]|->{y}]; last first.
   by split; [rewrite lb_set1|apply ub_lb_refl].
@@ -2674,12 +2708,14 @@ move=> x y [Ax xA] [Ay yA]; apply/eqP.
 by rewrite eq_le (lb_ub_lb Ax yA) (lb_ub_lb Ay xA).
 Qed.
 
+Definition infimum x0 A := if A == set0 then x0 else xget x0 (infimums A).
+
 End UpperLowerTheory.
 
 Section UpperLowerOrderTheory.
 Import Order.TTheory.
 Variables (d : unit) (T : orderType d).
-Implicit Types A : set T.
+Implicit Types (A : set T) (x y z : T).
 
 Lemma ge_supremum_Nmem x0 A t :
   supremums A !=set0 -> A t -> (supremum x0 A >= t)%O.
@@ -2706,8 +2742,6 @@ rewrite -Order.TotalTheory.ltNge => kn.
 by rewrite (Order.POrderTheory.le_trans _ (Am _ Ak)).
 Qed.
 
-(** ** Intersection of classes of set *)
-
 Definition meets T (F G : set (set T)) :=
   forall A B, F A -> G B -> A `&` B !=set0.
 

diff --git a/theories/ereal.v b/theories/ereal.v
@@ -2828,8 +2828,7 @@ End DualAddTheory.
 Section ereal_supremum.
 Variable R : realFieldType.
 Local Open Scope classical_set_scope.
-Implicit Types S : set (\bar R).
-Implicit Types x y : \bar R.
+Implicit Types (S : set (\bar R)) (x y : \bar R).
 
 Lemma ereal_ub_pinfty S : ubound S +oo.
 Proof. by apply/ubP=> x _; rewrite leey. Qed.
@@ -2860,15 +2859,9 @@ Definition ereal_sup S := supremum -oo S.
 
 Definition ereal_inf S := - ereal_sup (-%E @` S).
 
-Lemma ereal_sup0 : ereal_sup set0 = -oo.
-Proof. by rewrite /ereal_sup /supremum eqxx. Qed.
+Lemma ereal_sup0 : ereal_sup set0 = -oo. Proof. exact: supremum0. Qed.
 
-Lemma ereal_sup1 x : ereal_sup [set x] = x.
-Proof.
-rewrite /ereal_sup /supremum ifF; last first.
-  by apply/eqP; rewrite predeqE => /(_ x)[+ _]; apply.
-by rewrite supremums_set1; case: xgetP => // /(_ x) /(_ erefl).
-Qed.
+Lemma ereal_sup1 x : ereal_sup [set x] = x. Proof. exact: supremum1. Qed.
 
 Lemma ereal_inf0 : ereal_inf set0 = +oo.
 Proof. by rewrite /ereal_inf image_set0 ereal_sup0. Qed.
@@ -2888,23 +2881,21 @@ move=> SM; rewrite /ereal_inf lee_oppr; apply ub_ereal_sup => x [y Sy <-{x}].
 by rewrite lee_oppl oppeK; apply SM.
 Qed.
 
-Lemma ub_ereal_sup_adherent S (e : {posnum R}) :
-  ereal_sup S \is a fin_num -> exists x, S x /\ (ereal_sup S - e%:num%:E < x).
+Lemma ub_ereal_sup_adherent S (e : R) : (0 < e)%R ->
+  ereal_sup S \is a fin_num -> exists2 x, S x & (ereal_sup S - e%:E < x).
 Proof.
-move=> Sr.
-have : ~ ubound S (ereal_sup S - e%:num%:E).
+move=> e0 Sr; have : ~ ubound S (ereal_sup S - e%:E).
   move/ub_ereal_sup; apply/negP.
   by rewrite -ltNge lte_subl_addr // lte_addl // lte_fin.
 move/asboolP; rewrite asbool_neg; case/existsp_asboolPn => /= x.
-rewrite not_implyE => -[? ?]; exists x; split => //.
-by rewrite ltNge; apply/negP.
+by rewrite not_implyE => -[? ?]; exists x => //; rewrite ltNge; apply/negP.
 Qed.
 
-Lemma lb_ereal_inf_adherent S (e : {posnum R}) :
-  ereal_inf S \is a fin_num -> exists x, S x /\ (x < ereal_inf S + e%:num%:E).
+Lemma lb_ereal_inf_adherent S (e : R) : (0 < e)%R ->
+  ereal_inf S \is a fin_num -> exists2 x, S x & (x < ereal_inf S + e%:E).
 Proof.
-rewrite [in X in X -> _]/ereal_inf fin_numN => /(ub_ereal_sup_adherent e)[x []].
-move=> [y Sy <-]; rewrite -lte_oppr => /lt_le_trans ex; exists y; split => //.
+move=> e0; rewrite fin_numN => /(ub_ereal_sup_adherent e0)[x []].
+move=> y Sy <-; rewrite -lte_oppr => /lt_le_trans ex; exists y => //.
 by apply: ex; rewrite oppeD// oppeK.
 Qed.
 

diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -1146,7 +1146,7 @@ rewrite le_eqVlt => /predU1P[|] mufoo; last first.
   have : \int[mu]_x (f x) \is a fin_num.
     by rewrite ge0_fin_numE//; exact: integral_ge0.
   rewrite ge0_integralTE// => /ub_ereal_sup_adherent h.
-  apply: lee_adde => e; have {h}[/= _ [[G Gf <-]]] := h e.
+  apply: lee_adde => e; have {h} [/= _ [G Gf <-]] := h _ [gt0 of e%:num].
   rewrite EFinN lte_subl_addr// => fGe.
   have : forall x, cvg (g^~ x) -> (G x <= lim (g ^~ x))%R.
     move=> x cg; rewrite -lee_fin -(EFin_lim cg).

diff --git a/theories/measure.v b/theories/measure.v
@@ -2820,9 +2820,8 @@ have [G PG] : {G : ((set T)^nat)^nat & forall n, P n (G n)}.
   case: iS infS => [r Sr|Soo|Soo].
   - have en1 : (0 < e%:num / (2 ^ n.+1)%:R)%R.
       by rewrite divr_gt0 // ltr0n expn_gt0.
-    have /(lb_ereal_inf_adherent (PosNum en1)) : ereal_inf S \is a fin_num.
-      by rewrite Sr.
-    move=> [x [[B [mB AnB muBx]] xS]].
+    have /(lb_ereal_inf_adherent en1) : ereal_inf S \is a fin_num by rewrite Sr.
+    move=> [x [B [mB AnB muBx] xS]].
     exists B; split => //; rewrite muBx -Sr; apply/ltW.
     by rewrite (lt_le_trans xS) // lee_add2l //= lee_fin ler_pmul.
   - by have := Aoo n; rewrite /mu_ext Soo.