Supremums ereal

CHANGELOG_UNRELEASED.md

@@ -4,8 +4,23 @@
 
 ### Added
 
+- in `boolp.v`, lemmas for classical reasoning `existsNP`, `existsP`,
+  `forallNP`, `forallP`, `imply_classic`, `orC`.
+- in `classical_sets.v`, definitions for supremums: `ul`, `lb`,
+  `supremum`
+- in `ereal.v`:
+  + technical lemmas `lee_ninfty_eq`, `lee_pinfty_eq`, `lte_subl_addr`
+  + lemmas about supremum: `ereal_supremums_neq0`
+  + definitions:
+    * `ereal_sup`, `ereal_inf`
+  + lemmas about `ereal_sup`:
+    * `ereal_sup_ub`, `ub_ereal_sup`, `ub_ereal_sup_adherent`
+
 ### Changed
 
+- in `reals.v`, `pred` replaced by `set` from `classical_sets.v`
+  + change propagated in many files
+
 ### Renamed
 
 ### Removed

theories/Rstruct.v

@@ -374,44 +374,45 @@ Canonical R_rcfType := RcfType R Rreal_closed_axiom.
 End ssreal_struct.
 
 Local Open Scope ring_scope.
-Require Import reals boolp.
+Require Import reals boolp classical_sets.
 
 Section ssreal_struct_contd.
 
-Lemma is_upper_boundE (E : pred R) x : is_upper_bound E x = (x \in ub E).
+Lemma is_upper_boundE (E : set R) x : is_upper_bound E x = ((ub E) x).
 Proof.
-rewrite /is_upper_bound inE forallbE asboolE /=; apply/eq_forall=> y.
-by rewrite -(reflect_eq implyP) (reflect_eq (RleP _ _)).
+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 : pred R) : bound E = has_ub E.
+Lemma boundE (E : set R) : bound E = has_ub E.
 Proof. by apply/eq_exists=> x; rewrite is_upper_boundE. Qed.
 
-Lemma completeness' (E : pred R) : has_sup E -> {m : R | is_lub E m}.
+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 : pred R) : R :=
+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 : pred R) : has_sup E -> is_lub E (real_sup E).
+Lemma real_sup_is_lub (E : set R) : has_sup E -> is_lub E (real_sup E).
 Proof.
 by move=> hsE; rewrite /real_sup; case: pselect=> // ?; case: completeness'.
 Qed.
 
-Lemma real_sup_ub (E : pred R) : has_sup E -> real_sup E \in ub E.
+Lemma real_sup_ub (E : set R) : has_sup E -> (ub E) (real_sup E).
 Proof. by move=> /real_sup_is_lub []; rewrite is_upper_boundE. Qed.
 
-Lemma real_sup_out (E : pred R) : ~ has_sup E -> real_sup E = 0.
+Lemma real_sup_out (E : set R) : ~ has_sup E -> real_sup E = 0.
 Proof. by move=> nosup; rewrite /real_sup; case: pselect. 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 : pred R) (eps : R) :
+Lemma real_sup_adherent (E : set R) (eps : R) :
   has_sup E -> 0 < eps -> exists2 e : R, E e & (real_sup E - eps) < e.
 Proof.
 move=> supE eps_gt0; set m := _ - eps; apply: contrapT=> mNsmall.
-have: m \in ub E.
-  apply/ubP=> y Ey; have /negP := mNsmall (ex_intro2 _ _ y Ey _).
+have: (ub 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.

theories/altreals/distr.v

@@ -5,7 +5,7 @@
 
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect all_algebra.
-Require Import xfinmap boolp ereal reals discrete.
+Require Import xfinmap boolp classical_sets ereal reals discrete.
 Require Import realseq realsum.
 
 Set Implicit Arguments.
@@ -157,8 +157,8 @@ Qed.
 Local Lemma isd3 : psum mu <= 1.
 Proof.
 rewrite psumE; [apply/isd1 | apply/isd2 | apply/sup_le_ub].
-  by exists 0; apply/imsetbP; exists fset0; rewrite big_fset0.
-apply/ubP=> y /imsetbP[x ->]; rewrite big_fset_seq /=.
+  by exists 0, fset0; rewrite big_fset0.
+apply/ubP=> y [x ->]; rewrite big_fset_seq /=.
 by case: isd => _; apply; case: x => x /= /canonical_uniq.
 Qed.
 

theories/altreals/realseq.v

@@ -7,6 +7,7 @@
 From mathcomp Require Import all_ssreflect all_algebra.
 Require Import mathcomp.bigenough.bigenough.
 Require Import xfinmap boolp ereal reals discrete.
+Require Import classical_sets.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -213,7 +214,7 @@ Proof. by move=> le_uv; apply/(@ncvg_le_from 0). Qed.
 Lemma ncvg_nbounded u x : ncvg u x%:E -> nbounded u.
 Proof.                   (* FIXME: factor out `sup` of a finite set *)
 case/(_ (B x 1)) => K cu; pose S := [seq `|u n| | n <- iota 0 K].
-pose M : R := sup [pred x in S]; pose e := Num.max (`|x| + 1) (M + 1).
+pose M : R := sup [set x : R | x \in S]; pose e := Num.max (`|x| + 1) (M + 1).
 apply/asboolP/nboundedP; exists e => [|n]; first by rewrite ltxU ltr_paddl.
 case: (ltnP n K); last first.
   move/cu; rewrite inE eclamp_id ?ltr01 // => ltunBx1.
@@ -222,8 +223,8 @@ case: (ltnP n K); last first.
 move=> lt_nK; have: `|u n| \in S; first by apply/map_f; rewrite mem_iota.
 move=> un_S; rewrite ltxU; apply/orP; right.
 case E: {+}K lt_nK => [|k] // lt_nSk; apply/ltr_spaddr; first apply/ltr01.
-apply/sup_upper_bound; last by apply/map_f; rewrite mem_iota E.
-apply/has_supP; split; first by exists `|u 0%N|; rewrite /S E inE eqxx.
+suff : has_sup (fun x : R => x \in S) by move/sup_upper_bound/ubP => ->.
+split; first by exists `|u 0%N|; rewrite /S E inE eqxx.
 elim: {+}S => [|v s [ux /ubP hux]]; first by exists 0; apply/ubP.
 exists (Num.max v ux); apply/ubP=> y; rewrite inE => /orP[/eqP->|].
   by rewrite lexU lexx.
@@ -534,18 +535,18 @@ Qed.
 Lemma nlim_sup (u : nat -> R) l :
     (forall n m, (n <= m)%N -> u n <= u m)
   -> ncvg u l%:E
-  -> sup [pred r | `[exists n, r == u n]] = l.
+  -> sup [set r | exists n, r = u n] = l.
 Proof.
 move=> mn_u cv_ul; set S := (X in sup X); suff: ncvg u (sup S)%:E.
   by move/nlimE; move/nlimE: cv_ul => -> [->].
 elim/nbh_finW=> /= e gt0_e; have sS: has_sup S.
-  apply/has_supP; split; first exists (u 0%N).
-    by apply/imsetbP; exists 0%N.
-  exists l; apply/ubP => _ /imsetbP[n ->].
+  split; first exists (u 0%N).
+    by exists 0%N.
+  exists l; apply/ubP => _ [n ->].
   by rewrite -lee_fin; apply/ncvg_homo_le.
-have /sup_adherent := sS => /(_ _ gt0_e) [r /imsetbP] [N ->] lt_uN.
+have /sup_adherent := sS => /(_ _ gt0_e) [r] [N ->] lt_uN.
 exists N => n le_Nn; rewrite !inE distrC ger0_norm ?subr_ge0.
-  by apply/sup_upper_bound => //; apply/imsetbP; exists n.
+  by move/ubP : (sup_upper_bound sS) => -> //; exists n.
 by rewrite ltr_subl_addr -ltr_subl_addl (lt_le_trans lt_uN) ?mn_u.
 Qed.