fixes #1046

CHANGELOG_UNRELEASED.md

@@ -4,6 +4,9 @@
 
 ### Added
 
+- in `constructive_ereal.v`:
+  + lemmas `gt0_fin_numE`, `ltr0_fin_numE`
+
 ### Changed
 
 - in `hoelder.v`:

theories/charge.v

@@ -471,8 +471,7 @@ have := d_ge0 A; rewrite le_eqVlt => /predU1P[<-|d_gt0].
 have /ereal_sup_gt/cid2[_ [B/= [mB BDA <- mnuB]]] : m < d_ A.
   rewrite /m; have [->|dn1oo] := eqVneq (d_ A) +oo.
     by rewrite min_r ?ltey ?gt0_mulye ?leey.
-  rewrite -(@fineK _ (d_ A)); last first.
-    by rewrite ge0_fin_numE// ?(ltW d_gt0)// lt_neqAle dn1oo leey.
+  rewrite -(@fineK _ (d_ A)); last by rewrite gt0_fin_numE// ltey.
   rewrite -EFinM -fine_min// lte_fin lt_minl; apply/orP; left.
   by rewrite ltr_pdivr_mulr// ltr_pmulr ?ltr1n// fine_gt0// d_gt0/= ltey.
 by exists B; split => //; rewrite (le_trans _ (ltW mnuB)).
@@ -649,8 +648,7 @@ have := s_le0 U; rewrite le_eqVlt => /predU1P[->|s_lt0].
 have /ereal_inf_lt/cid2[_ [B/= [mB BU] <-] nuBm] : s_ U < m.
   rewrite /m; have [->|s0oo] := eqVneq (s_ U) -oo.
     by rewrite max_r ?ltNye// gt0_mulNye// leNye.
-  rewrite -(@fineK _ (s_ U)); last first.
-    by rewrite le0_fin_numE// ?(ltW s_lt0)// lt_neqAle leNye eq_sym s0oo.
+  rewrite -(@fineK _ (s_ U)); last by rewrite lt0_fin_numE// ltNye.
   rewrite -EFinM -fine_max// lte_fin lt_maxr; apply/orP; left.
   by rewrite ltr_pdivl_mulr// gtr_nmulr ?ltr1n// fine_lt0// s_lt0/= ltNye andbT.
 have [C [CB nsC nuCB]] := hahn_decomposition_lemma nu mB.

theories/constructive_ereal.v

@@ -1468,9 +1468,15 @@ Proof. by case: x => // x //=; exact: ltNyr. Qed.
 Lemma ge0_fin_numE x : 0 <= x -> (x \is a fin_num) = (x < +oo).
 Proof. by move: x => [x| |] => // x0; rewrite fin_numElt ltNyr. Qed.
 
+Lemma gt0_fin_numE x : 0 < x -> (x \is a fin_num) = (x < +oo).
+Proof. by move/ltW; exact: ge0_fin_numE. Qed.
+
 Lemma le0_fin_numE x : x <= 0 -> (x \is a fin_num) = (-oo < x).
 Proof. by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed.
 
+Lemma lt0_fin_numE x : x < 0 -> (x \is a fin_num) = (-oo < x).
+Proof. by move/ltW; exact: le0_fin_numE. Qed.
+
 Lemma eqyP x : x = +oo <-> (forall A, (0 < A)%R -> A%:E <= x).
 Proof.
 split=> [-> // A A0|Ax]; first by rewrite leey.

theories/hoelder.v

@@ -173,7 +173,7 @@ have foo : \int[mu]_x (`|f x| `^ p)%:E < +oo.
   move/integrableP: ifp => -[_].
   by under eq_integral do rewrite gee0_abs// ?lee_fin ?powR_ge0//.
 rewrite integralZl//; apply/eqP; rewrite eqe_pdivr_mull ?mule1.
-- by rewrite fineK// ge0_fin_numE// ltW.
+- by rewrite fineK// gt0_fin_numE.
 - by rewrite gt_eqF// fine_gt0// foo andbT.
 Qed.
 

theories/lebesgue_integral.v

@@ -1090,8 +1090,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
   by move/cvg_lim => -> //; apply: ereal_sup_ub; exists n.
 have := leey (\int[mu]_x (f x)).
 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.
+  have : \int[mu]_x (f x) \is a fin_num by rewrite ge0_fin_numE// integral_ge0.
   rewrite ge0_integralTE// => /ub_ereal_sup_adherent h.
   apply/lee_addgt0Pr => _/posnumP[e].
   have {h} [/= _ [G Gf <-]] := h _ [gt0 of e%:num].
@@ -1275,7 +1274,7 @@ Let fpos_approx_neq0 x : D x -> (0%E < f x < +oo)%E ->
   \forall n \near \oo, approx n x != 0.
 Proof.
 move=> Dx /andP[fx_gt0 fxoo].
-have fxfin : f x \is a fin_num by rewrite ge0_fin_numE// ltW.
+have fxfin : f x \is a fin_num by rewrite gt0_fin_numE.
 rewrite -(fineK fxfin) lte_fin in fx_gt0; near=> n.
 rewrite /approx paddr_eq0//; last 2 first.
   by apply: sumr_ge0 => i _; rewrite mulr_ge0.
@@ -1421,7 +1420,7 @@ have cvg_af := cvg_approx fi0 Dx fixoo.
 have is_cvg_af : cvg (approx ^~ x) by apply/cvg_ex; eexists; exact: cvg_af.
 have {is_cvg_af} := nondecreasing_cvg_le nd_ag is_cvg_af k.
 rewrite -lee_fin => /le_trans; apply.
-rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE //; apply: f0.
+rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE// f0.
 by move/(cvg_lim (@Rhausdorff R)) : cvg_af => ->.
 Qed.
 
@@ -1720,7 +1719,7 @@ move=> D [/= mD Deps KDf]; exists (K `\` D); split => //.
     by apply: measureU2 => //; apply: measurableI => //; apply: measurableC.
   rewrite [_%:num]splitr EFinD; apply: lee_lt_add => //=; first 2 last.
   + by rewrite (@le_lt_trans _ _ (mu D)) ?le_measure ?inE//; exact: measurableI.
-  + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure// ?inE//.
+  + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure ?inE//.
     exact: measurableD.
   rewrite setDE setC_bigcap setI_bigcupr.
   apply: (@le_trans _ _(\sum_(k <oo) mu (A `\` gK k))).
@@ -2450,10 +2449,9 @@ rewrite monotone_convergence //.
     exists 1%N => // m /= m0; move: muDoo; rewrite leye_eq => /eqP ->.
     by rewrite mulry gtr0_sg ?mul1e ?leey// ltr0n.
   exists `|ceil (M / fine (mu D))|%N => // m /=.
-  rewrite -(ler_nat R) => MDm.
-  rewrite -(@fineK _ (mu D)); last by rewrite ge0_fin_numE.
+  rewrite -(ler_nat R) => MDm; rewrite -(@fineK _ (mu D)) ?ge0_fin_numE//.
   rewrite -lee_pdivr_mulr; last by rewrite fine_gt0// lt0e muD0 measure_ge0.
-  rewrite lee_fin; apply: le_trans MDm.
+  rewrite lee_fin (le_trans _ MDm)//.
   by rewrite natr_absz (le_trans (ceil_ge _))// ler_int ler_norm.
 - by move=> n; exact: measurable_cst.
 - by move=> n x Dx; rewrite lee_fin.
@@ -3211,7 +3209,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
     - by move=> *; rewrite lee_fin.
   rewrite fineK//; last first.
     case: (integrableP _ _ _ fint) => _ foo.
-    by rewrite ge0_fin_numE//; exact: integral_ge0.
+    by rewrite ge0_fin_numE// integral_ge0.
   apply: ge0_le_integral => //.
   - by move=> *; rewrite lee_fin /indic.
   - exact/EFin_measurable_fun/measurableT_comp.
@@ -3303,7 +3301,7 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) +
       \int[mu]_(x in D) (g1^\+ x) + \int[mu]_(x in D) (g2^\+ x) \is a fin_num.
     rewrite ge0_fin_numE//.
       by rewrite lte_add_pinfty//; exact: integral_funepos_lt_pinfty.
-    by apply: adde_ge0; exact: integral_ge0.
+    by rewrite adde_ge0// integral_ge0.
   have g12neg :
       \int[mu]_(x in D) (g1^\- x) + \int[mu]_(x in D) (g2^\- x) \is a fin_num.
     rewrite ge0_fin_numE//.
@@ -3313,9 +3311,8 @@ suff: \int[mu]_(x in D) ((g1 \+ g2)^\+ x) + \int[mu]_(x in D) (g1^\- x) +
     - rewrite ge0_fin_numE.
         apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
         apply: lte_add_pinfty; last exact: integral_funeneg_lt_pinfty.
-        have : mu.-integrable D (g1 \+ g2) by apply: integrableD.
-        exact: integral_funepos_lt_pinfty.
-      apply: adde_ge0; last exact: integral_ge0.
+        exact: integral_funepos_lt_pinfty (integrableD _ _ _).
+      rewrite adde_ge0//; last exact: integral_ge0.
       by apply: adde_ge0; exact: integral_ge0.
     - by rewrite fin_num_adde_defr.
   rewrite -(addeA (\int[mu]_(x in D) (g1 \+ g2)^\+ x)).
@@ -4548,8 +4545,7 @@ have m2Fn_bounded : exists M, forall X, measurable X -> (m2Fn X < M%:E)%E.
   exists (fine (m2Fn (F n)) + 1) => Y mY.
   rewrite [in ltRHS]EFinD lte_spadder// fineK; last first.
     by rewrite ge0_fin_numE ?measure_ge0//= /mrestr/= setIid.
-  rewrite /= /mrestr/= setIid; apply: le_measure => //; rewrite inE//.
-  exact: measurableI.
+  by rewrite /= /mrestr/= setIid le_measure// inE//; exact: measurableI.
 pose phi' A := m2Fn \o xsection A.
 pose B' := [set A | measurable A /\ measurable_fun setT (phi' A)].
 have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_xsection.
@@ -4584,8 +4580,7 @@ have m1Fn_bounded : exists M, forall X, measurable X -> (m1Fn X < M%:E)%E.
   exists (fine (m1Fn (F n)) + 1) => Y mY.
   rewrite [in ltRHS]EFinD lte_spadder// fineK; last first.
     by rewrite ge0_fin_numE ?measure_ge0// /m1Fn/= /mrestr setIid.
-  rewrite /m1Fn/= /mrestr setIid; apply: le_measure => //; rewrite inE//=.
-  exact: measurableI.
+  by rewrite /m1Fn/= /mrestr setIid le_measure// inE//=; exact: measurableI.
 pose psi' A := m1Fn \o ysection A.
 pose B' := [set A | measurable A /\ measurable_fun setT (psi' A)].
 have subset_B' : measurable `<=` B' by exact: measurable_prod_subset_ysection.

theories/measure.v

@@ -2975,7 +2975,7 @@ Let mnormalize1 : mnormalize [set: T] = 1.
 Proof.
 rewrite /mnormalize; case: ifPn; first by rewrite probability_setT.
 rewrite negb_or => /andP[ft0 ftoo].
-have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// lt_neqAle ftoo/= leey.
+have ? : mu setT \is a fin_num by rewrite ge0_fin_numE// ltey.
 by rewrite -{1}(@fineK _ (mu setT))// -EFinM divrr// ?unitfE fine_eq0.
 Qed.
 

theories/normedtype.v

@@ -3795,7 +3795,7 @@ Qed.
 Lemma edist_pinfty_open : open [set xy : X * X | edist xy = +oo]%E.
 Proof.
 rewrite -closedC; have := edist_fin_closed; congr (_ _).
-by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE // ltey; move/eqP.
+by rewrite eqEsubset; split => z; rewrite /= ?ge0_fin_numE// ltey => /eqP.
 Qed.
 
 Lemma edist_sym (x y : X) : edist (x, y) = edist (y, x).
@@ -4034,11 +4034,11 @@ Section topological_urysohn_separator.
 Context {T : topologicalType} {R : realType}.
 
 Definition uniform_separator (A B : set T) :=
-  exists (uT : @Uniform.class_of T^o) (E : set (T * T)), 
-    let UT := Uniform.Pack uT in [/\ 
+  exists (uT : @Uniform.class_of T^o) (E : set (T * T)),
+    let UT := Uniform.Pack uT in [/\
       @entourage UT E, A `*` B `&` E = set0 &
       (forall x, @nbhs UT UT x `<=` @nbhs T T x)].
-    
+
 Local Lemma Urysohn' (A B : set T) : exists (f : T -> R),
     [/\ continuous f,
     range f `<=` `[0, 1]