lemmas on ereal.v from lspace_master

CHANGELOG_UNRELEASED.md

@@ -69,13 +69,21 @@
 
 - file `lebesgue_integral_approximation.v` -> `measurable_fun_approximation.v`
 
+- in `ereal.v`:
+  + `ereal_sup_le` -> `ereal_sup_ge`
+
 ### Generalized
 
 - in `normedtype.v`:
   + lemmas `gt0_cvgMlNy`, `gt0_cvgMly`
 - in `functions.v`:
   + `fct_sumE`, `addrfctE`, `sumrfctE` (from `zmodType` to `nmodType`)
   + `scalerfctE` (from `pointedType` to `Type`)
+- in `ereal.v`:
+  + lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN`
+  + lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`,
+    `ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`,
+    `ereal_sup_real`, `ereal_inf_real`
 
 ### Deprecated
 

theories/ereal.v

@@ -9,7 +9,7 @@ From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import fsbigop cardinality set_interval.
 From mathcomp Require Import reals interval_inference topology.
-From mathcomp Require Export constructive_ereal.
+From mathcomp Require Export constructive_ereal unstable.
 
 (**md**************************************************************************)
 (* # Extended real numbers, classical part ($\overline{\mathbb{R}}$)          *)
@@ -463,6 +463,21 @@ rewrite lteNl => /ereal_sup_gt[_ [y Sy <-]].
 by rewrite lteNl oppeK => xlty; exists y.
 Qed.
 
+Lemma ereal_infEN S : ereal_inf S = - ereal_sup (-%E @` S).
+Proof. by []. Qed.
+
+Lemma ereal_supN S : ereal_sup (-%E @` S) = - ereal_inf S.
+Proof. by rewrite oppeK. Qed.
+
+Lemma ereal_infN S : ereal_inf (-%E @` S) = - ereal_sup S.
+Proof.
+rewrite /ereal_inf; congr (- ereal_sup _) => /=.
+by rewrite image_comp -[RHS]image_id; apply: eq_imagel => /= ?; rewrite oppeK.
+Qed.
+
+Lemma ereal_supEN S : ereal_sup S = - ereal_inf (-%E @` S).
+Proof. by rewrite ereal_infN oppeK. Qed.
+
 End ereal_supremum.
 
 Section ereal_supremum_realType.
@@ -523,7 +538,7 @@ Proof.
 by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ubound.
 Qed.
 
-Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
+Lemma ereal_sup_ge S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
 Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ubound. Qed.
 
 Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo].
@@ -591,11 +606,83 @@ rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN].
 by rewrite !image_comp.
 Qed.
 
+Lemma ereal_supP S x :
+  reflect (forall y : \bar R, S y -> y <= x) (ereal_sup S <= x).
+Proof.
+apply/(iffP idP) => [+ y Sy|].
+  by move=> /(le_trans _)->//; rewrite ereal_sup_ge//; exists y.
+apply: contraPP => /negP; rewrite -ltNge -existsPNP.
+by move=> /ereal_sup_gt[y Sy ltyx]; exists y => //; rewrite lt_geF.
+Qed.
+
+Lemma ereal_infP S x :
+  reflect (forall y : \bar R, S y -> x <= y) (x <= ereal_inf S).
+Proof.
+rewrite leeNr; apply/(equivP (ereal_supP _ _)); setoid_rewrite leeNr.
+split=> [ge_x y Sy|ge_x _ [y Sy <-]]; rewrite ?oppeK// ?ge_x//.
+by rewrite -[y]oppeK ge_x//; exists y.
+Qed.
+
+Lemma ereal_sup_gtP S x :
+  reflect (exists2 y : \bar R, S y & x < y) (x < ereal_sup S).
+Proof.
+rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_supP _ _)) -existsPNP.
+by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge.
+Qed.
+
+Lemma ereal_inf_ltP S x :
+  reflect (exists2 y : \bar R, S y & y < x) (ereal_inf S < x).
+Proof.
+rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_infP _ _)) -existsPNP.
+by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge.
+Qed.
+
+Lemma ereal_inf_leP S x : S (ereal_inf S) ->
+  reflect (exists2 y : \bar R, S y & y <= x) (ereal_inf S <= x).
+Proof.
+move=> Sinf; apply: (iffP idP); last exact: ereal_inf_le.
+by move=> Sx; exists (ereal_inf S).
+Qed.
+
+Lemma ereal_sup_geP S x : S (ereal_sup S) ->
+  reflect (exists2 y : \bar R, S y & x <= y) (x <= ereal_sup S).
+Proof.
+move=> Ssup; apply: (iffP idP); last exact: ereal_sup_ge.
+by move=> Sx; exists (ereal_sup S).
+Qed.
+
+Lemma lb_ereal_infNy_adherent S e :
+  ereal_inf S = -oo -> exists2 x : \bar R, S x & x < e%:E.
+Proof. by move=> infNy; apply/ereal_inf_ltP; rewrite infNy ltNyr. Qed.
+
+Lemma ereal_sup_real : @ereal_sup R (range EFin) = +oo.
+Proof.
+rewrite hasNub_ereal_sup//; last by exists 0%R.
+by apply/has_ubPn => x; exists (x+1)%R => //; rewrite ltrDl.
+Qed.
+
+Lemma ereal_inf_real : @ereal_inf R (range EFin) = -oo.
+Proof.
+rewrite /ereal_inf [X in ereal_sup X](_ : _ = range EFin); last first.
+  apply/seteqP; split => x/=[y].
+    by move=> [z] _ <- <-; exists (-z)%R.
+  by move=> _ <-; exists (-y%:E); first (by exists (-y)%R); rewrite oppeK.
+by rewrite ereal_sup_real.
+Qed.
+
 End ereal_supremum_realType.
 #[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_sup_ubound`.")]
 Notation ereal_sup_ub := ereal_sup_ubound (only parsing).
 #[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_inf_lbound`.")]
 Notation ereal_inf_lb := ereal_inf_lbound (only parsing).
+#[deprecated(since="mathcomp-analysis 1.11.0", note="Renamed `ereal_sup_ge`.")]
+Notation ereal_sup_le := ereal_sup_ge.
+Arguments ereal_supP {R S x}.
+Arguments ereal_infP {R S x}.
+Arguments ereal_sup_gtP {R S x}.
+Arguments ereal_inf_ltP {R S x}.
+Arguments ereal_sup_geP {R S x}.
+Arguments ereal_inf_leP {R S x}.
 
 Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) :
   (abse \o f) \_ D = abse \o (f \_ D).

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -424,11 +424,10 @@ Local Notation HL := HL_maximal.
 Lemma HL_maximal_ge0 f D : locally_integrable D f ->
   forall x, 0 <= HL (f \_ D) x.
 Proof.
-move=> Df x; apply: ereal_sup_le => //=.
+move=> Df x; apply: ereal_sup_ge => //=.
 pose k := \int[mu]_(x in D `&` ball x 1) `|f x|%:E.
 exists ((fine (mu (ball x 1)))^-1%:E * k); last first.
-  rewrite mule_ge0 ?integral_ge0//.
-  by rewrite lee_fin// invr_ge0// fine_ge0.
+  by rewrite mule_ge0 ?integral_ge0// lee_fin// invr_ge0// fine_ge0.
 exists 1%R; first by rewrite in_itv/= ltr01.
 rewrite iavg_restrict//; last exact: measurable_ball.
 by case: Df => _ /open_measurable.

theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v

@@ -1083,10 +1083,9 @@ rewrite -ge0_integral_bigsetU//=; first last.
 rewrite big_mkord -bigsetU_seqDU.
 move: n => [|n].
   rewrite big_ord0 integral_set0.
-  apply: ereal_sup_le.
+  apply: ereal_sup_ge.
   exists (\int[mu]_(x in `[0%R, 1%:R]) (f x)%:E) => //.
-  apply: integral_ge0.
-  by move=> ? _; rewrite lee_fin f0.
+  by apply: integral_ge0 => /= ? _; rewrite lee_fin f0.
 rewrite [X in \int[_]_(_ in X) _](_ : _ = `[0%R, n.+1%:R]%classic); last first.
   rewrite eqEsubset; split => x/=; rewrite in_itv/=.
     rewrite -(bigcup_mkord _ (fun k => `[0%R, k.+1%:R]%classic)).
@@ -1097,7 +1096,7 @@ rewrite [X in \int[_]_(_ in X) _](_ : _ = `[0%R, n.+1%:R]%classic); last first.
   rewrite -(bigcup_mkord _ (fun k => `[0%R, k.+1%:R]%classic)).
   exists n => //=.
   by rewrite in_itv/= x0 Snx.
-apply: ereal_sup_le.
+apply: ereal_sup_ge.
 exists (\int[mu]_(x in `[0%R, n.+1%:R]) (f x)%:E); first by exists n.
 apply: ge0_subset_integral => //= [|? _]; last by rewrite lee_fin f0.
 exact/measurable_EFinP/measurableT_comp.

theories/realfun.v

@@ -989,9 +989,9 @@ Qed.
 Lemma lime_inf_sup f a : lime_inf f a <= lime_sup f a.
 Proof.
 rewrite lime_inf_lim lime_sup_lim; apply: lee_lim => //.
-near=> r; rewrite ereal_sup_le//.
-have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2)%R.
-  exists (a + r / 2)%R => //; split.
+near=> r; rewrite ereal_sup_ge//.
+have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2).
+  exists (a + r / 2) => //; split.
     rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//.
     by rewrite ltr_pdivrMr// ltr_pMr// ltr1n.
   by apply/eqP; rewrite gt_eqF// ltr_pwDr// divr_gt0.
@@ -2316,7 +2316,7 @@ Lemma total_variationN a b f : TV a b (\- f) = TV a b f.
 Proof. by rewrite /TV; rewrite variationsN. Qed.
 
 Lemma total_variation_le a b f g : a <= b ->
-  (TV a b (f \+ g)%R <= TV a b f + TV a b g)%E.
+  (TV a b (f \+ g) <= TV a b f + TV a b g)%E.
 Proof.
 rewrite le_eqVlt => /predU1P[<-{b}|ab].
   by rewrite !total_variationxx adde0.
@@ -2336,7 +2336,7 @@ have BVabfg : BV a b (f \+ g).
 apply: ub_ereal_sup => y /= [r' [s' abs <-{r'} <-{y}]].
 apply: (@le_trans _ _ (variation a b f s' + variation a b g s')%:E).
   exact: variation_le.
-by rewrite EFinD leeD// ereal_sup_le//;
+by rewrite EFinD leeD// ereal_sup_ge//;
   (eexists; last exact: lexx); (eexists; last reflexivity);
   exact: variations_variation.
 Qed.
@@ -2351,7 +2351,7 @@ have [abf|abf] := pselect (BV a b f); last first.
   by apply: variations_neq0 => //; rewrite (lt_trans ac).
 have H s t : itv_partition a c s -> itv_partition c b t ->
     (TV a b f >= (variation a c f s)%:E + (variation c b f t)%:E)%E.
-  move=> acs cbt; rewrite -EFinD; apply: ereal_sup_le.
+  move=> acs cbt; rewrite -EFinD; apply: ereal_sup_ge.
   exists (variation a b f (s ++ t))%:E.
     eexists; last reflexivity.
     by exists (s ++ t) => //; exact: itv_partition_cat acs cbt.
@@ -2383,13 +2383,13 @@ rewrite le_eqVlt => /predU1P[<-{b}|cb]; first by rewrite total_variationxx adde0
 case : (pselect (bounded_variation a c f)); first last.
   move=> nbdac; have /eqP -> : TV a c f == +oo%E.
     have: (-oo < TV a c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f (ltW ac))).
-    by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW ac)).
+    by rewrite ltNye_eq => /orP[|//] => /bounded_variationP => /(_ (ltW ac)).
   by rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 // ltW.
-case : (pselect (bounded_variation c b f)); first last.
-  move=> nbdac; have /eqP -> : TV c b f == +oo%E.
+have [|nbdac] := pselect (bounded_variation c b f); first last.
+  have /eqP -> : TV c b f == +oo%E.
     have: (-oo < TV c b f)%E.
       exact: (lt_le_trans _ (total_variation_ge0 f (ltW cb))).
-    by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW cb)).
+    by rewrite ltNye_eq => /orP[|//] => /bounded_variationP => /(_ (ltW cb)).
   rewrite addey ?leey // -ltNye (@lt_le_trans _ _ 0%E)//.
   exact/total_variation_ge0/ltW.
 move=> bdAB bdAC.
@@ -2402,7 +2402,7 @@ apply: (le_trans (variation_itv_partitionLR _ ac _ _)) => //.
 apply: sup_ubound => /=.
   case: bdAB => M ubdM; case: bdAC => N ubdN; exists (N + M).
   move=> q [?] [i pabi <-] [? [j pbcj <-]] <-.
-  by apply: lerD; [apply: ubdN;exists i|apply:ubdM;exists j].
+  by apply: lerD; [apply: ubdN; exists i|apply: ubdM; exists j].
 exists (variation a c f (itv_partitionL l c)).
   by apply: variations_variation; exact: itv_partitionLP pacl.
 exists (variation c b f (itv_partitionR l c)).