lee_addgt0Pr

CHANGELOG_UNRELEASED.md

@@ -10,6 +10,9 @@
 ### Changed
 
 - `mnormalize` moved from `kernel.v` to `measure.v` and generalized
+- in `constructive_ereal.v`:
+  + `lee_adde` renamed to `lee_addgt0Pr` and turned into a reflect
+  + `lee_dadde` renamed to `lee_daddgt0Pr` and turned into a reflect
 
 ### Renamed
 

theories/constructive_ereal.v

@@ -2999,17 +2999,16 @@ Variable R : realFieldType.
 Implicit Types x y : \bar R.
 Implicit Types r : R.
 
-Lemma lee_adde x y : (forall e : {posnum R}, x <= y + e%:num%:E) -> x <= y.
+Lemma lee_addgt0Pr x y :
+  reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).
 Proof.
-move: x y => [x||] [y||] // xleye; rewrite ?leNye ?leey//; last first.
-- exact: (le_trans (xleye 1%:pos%R)).
-- by move: (!! xleye 1%:pos%R).
-- by move: (!! xleye 1%:pos%R).
-rewrite leNgt; apply/negP => yltx.
-have xmy_gt0 : (0 < (x - y) / 2)%R by rewrite ltr_pdivl_mulr// mul0r subr_gt0.
-move: (xleye (PosNum xmy_gt0)); apply/negP; rewrite -ltNge /= -EFinD lte_fin.
-rewrite [Y in (Y + _)%R]splitr [X in (_ < X)%R]splitr.
-by rewrite -!mulrDl ltr_pmul2r// addrCA addrK ltr_add2l.
+apply/(iffP idP) => [|].
+- move: x y => [x| |] [y| |]//.
+  + by rewrite lee_fin => xy e e0; rewrite -EFinD lee_fin ler_paddr// ltW.
+  + by move=> _ e e0; rewrite leNye.
+- move: x y => [x| |] [y| |]// xy; rewrite ?leey ?leNye//;
+    [|by move: xy => /(_ _ lte01)..].
+  by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy.
 Qed.
 
 Lemma lee_mul01Pr x y : 0 <= x ->
@@ -3141,8 +3140,9 @@ Local Open Scope ereal_dual_scope.
 Variable R : realFieldType.
 Implicit Types x y : \bar R.
 
-Lemma lee_dadde x y : (forall e : {posnum R}, x <= y + e%:num%:E) -> x <= y.
-Proof. by move=> xye; apply: lee_adde => e; case: x {xye} (xye e). Qed.
+Lemma lee_daddgt0Pr x y :
+  reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).
+Proof. exact: lee_addgt0Pr. Qed.
 
 End DualRealFieldType_lemmas.
 

theories/lebesgue_integral.v

@@ -1075,7 +1075,8 @@ 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 _ [gt0 of e%:num].
+  apply/lee_addgt0Pr => _/posnumP[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).

theories/lebesgue_measure.v

@@ -339,7 +339,7 @@ Proof.
 move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE.
 move=> [a _ <-]; rewrite hlength_itv ?lte_fin/= -EFinB => lebig.
 case: ifPn => a12; last by rewrite nneseries_esum// esum_ge0.
-apply: lee_adde => e.
+apply/lee_addgt0Pr => _ /posnumP[e].
 rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//.
 apply: le_trans (epsilon_trick _ _ _) => //=.
 have eVn_gt0 n : 0 < e%:num / 2 / (2 ^ n.+1)%:R.

theories/measure.v

@@ -3727,7 +3727,7 @@ move=> A; have [[i ioo]|] := pselect (exists i, mu^* (A i) = +oo).
 rewrite -forallNE => Aoo.
 suff add2e (e : {posnum R}) :
     mu^* (\bigcup_n A n) <= \sum_(i <oo) mu^* (A i) + e%:num%:E.
-  exact: lee_adde.
+  by apply/lee_addgt0Pr => _/posnumP[].
 rewrite (le_trans _ (epsilon_trick _ _ _))//; last first.
   by move=> n; exact: mu_ext_ge0.
 pose P n (B : (set T)^nat) := measurable_cover (A n) B /\

theories/normedtype.v

@@ -3809,7 +3809,7 @@ have [fyn|] := boolP (edist_inf y \is a fin_num); first last.
   by rewrite ge0_fin_numE// ?ltey// negbK => /eqP->; rewrite addey ?leey.
 have [xyfin|] := boolP (edist (x, y) \is a fin_num); first last.
   by rewrite ge0_fin_numE// ?ltey // negbK => /eqP->; rewrite addye ?leey.
-apply: lee_adde => eps.
+apply/lee_addgt0Pr => _/posnumP[eps].
 have [//|? [a Aa <-] yaeps] := @lb_ereal_inf_adherent R _ eps%:num _ fyn.
 apply: le_trans; first by apply: (@ereal_inf_lb _ _ (edist (x, a))); exists a.
 apply: le_trans; first exact: (@edist_triangle _ _ _ y).