From 32ed969858f209647b11ed14ebdfee084dde3034 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 27 Jul 2023 15:19:01 +0900 Subject: [PATCH] lee_addgt0Pr --- CHANGELOG_UNRELEASED.md | 3 +++ theories/constructive_ereal.v | 24 ++++++++++++------------ theories/lebesgue_integral.v | 3 ++- theories/lebesgue_measure.v | 2 +- theories/measure.v | 2 +- theories/normedtype.v | 2 +- 6 files changed, 20 insertions(+), 16 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c45275000f..108f2dda43 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 59770fbc6d..67caa09529 100644 --- a/theories/constructive_ereal.v +++ b/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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 788f928d0d..5828b96907 100644 --- a/theories/lebesgue_integral.v +++ b/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). diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 08a223d7ac..3e42778b11 100644 --- a/theories/lebesgue_measure.v +++ b/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. diff --git a/theories/measure.v b/theories/measure.v index 324d864170..a90058e0b0 100644 --- a/theories/measure.v +++ b/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 _/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 /\ diff --git a/theories/normedtype.v b/theories/normedtype.v index a8ddcbf8e1..7d0e15850b 100644 --- a/theories/normedtype.v +++ 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).