Co-authored-by: Pierre Roux <pierre@roux01.fr>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -5,17 +5,23 @@
 ### Added
 
 - in `ereal.v`:
+  + notations `_ < _ :> _` and `_ <= _ :> _`
   + lemmas `lee01`, `lte01`, `lee0N1`, `lte0N1`
   + lemmas `lee_pmul2l`, `lee_pmul2r`, `lte_pmul`, `lee_wpmul2l`
-  + lemmas `lee_lt_add`, `lee_paddl`, `lte_addl`, `lee_paddr`, `lte_paddr`, `lee_lt_add`
+  + lemmas `lee_lt_add`, `lee_paddl`, `lte_addl`, `lee_paddr`, `lte_paddr`
 
 ### Changed
 
 - in `ereal.v`:
   + generalize `lee_pmul`
+  + simplify `lte_le_add`, `lte_le_dsub`
 
 ### Renamed
 
+- in `ereal.v`:
+  + `lee_pinfty_eq` -> `leye_eq`
+  + `lee_ninfty_eq` -> `leeNy_eq`
+
 ### Removed
 
 ### Infrastructure

theories/ereal.v

@@ -311,6 +311,9 @@ Notation "x <= y < z"  := ((x <= y) && (y < z)) : ereal_scope.
 Notation "x < y < z"   := ((x < y) && (y < z)) : ereal_dual_scope.
 Notation "x < y < z"   := ((x < y) && (y < z)) : ereal_scope.
 
+Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : ereal_scope.
+Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing) : ereal_scope.
+
 Section ERealOrder_numDomainType.
 Context {R : numDomainType}.
 Implicit Types x y : \bar R.
@@ -319,13 +322,13 @@ Lemma lee_fin (r s : R) : (r%:E <= s%:E) = (r <= s)%R. Proof. by []. Qed.
 
 Lemma lte_fin (r s : R) : (r%:E < s%:E) = (r < s)%R. Proof. by []. Qed.
 
-Lemma lee01 : 0 <= (1 : \bar R). Proof. by rewrite lee_fin. Qed.
+Lemma lee01 : 0 <= 1 :> \bar R. Proof. by rewrite lee_fin. Qed.
 
-Lemma lte01 : 0 < (1 : \bar R). Proof. by rewrite lte_fin. Qed.
+Lemma lte01 : 0 < 1 :> \bar R. Proof. by rewrite lte_fin. Qed.
 
-Lemma lee_ninfty_eq x : (x <= -oo) = (x == -oo). Proof. by case: x. Qed.
+Lemma leeNy_eq x : (x <= -oo) = (x == -oo). Proof. by case: x. Qed.
 
-Lemma lee_pinfty_eq x : (+oo <= x) = (x == +oo). Proof. by case: x. Qed.
+Lemma leye_eq x : (+oo <= x) = (x == +oo). Proof. by case: x. Qed.
 
 Lemma lt0y : (0 : \bar R) < +oo. Proof. exact: real0. Qed.
 
@@ -345,6 +348,8 @@ Qed.
 
 End ERealOrder_numDomainType.
 
+#[global] Hint Resolve lee01 lte01 : core.
+
 Section ERealOrder_realDomainType.
 Context {R : realDomainType}.
 Implicit Types (x y : \bar R) (r : R).
@@ -526,10 +531,10 @@ Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) :=
 Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) ident(z) :=
   by case: x y z => [?||] [?||] [?||]; first by rewrite ?eqe; apply: lm.
 
-Lemma lee0N1 : (0 : \bar R) <= (-1)%:E = false.
+Lemma lee0N1 : 0 <= (-1)%:E :> \bar R = false.
 Proof. by rewrite lee_fin ler0N1. Qed.
 
-Lemma lte0N1 : (0 : \bar R) < (-1)%:E = false.
+Lemma lte0N1 : 0 < (-1)%:E :> \bar R = false.
 Proof. by rewrite lte_fin ltr0N1. Qed.
 
 Lemma le0R x : 0 <= x -> (0 <= fine x)%R.
@@ -1312,7 +1317,7 @@ Context {R : realDomainType}.
 Implicit Types (x y z u a b : \bar R) (r : R).
 
 Lemma fin_numElt x : (x \is a fin_num) = (-oo < x < +oo).
-Proof. by rewrite fin_numE -lee_pinfty_eq -lee_ninfty_eq -2!ltNge. Qed.
+Proof. by rewrite fin_numE -leye_eq -leeNy_eq -2!ltNge. Qed.
 
 Lemma fin_numPlt x : reflect (-oo < x < +oo) (x \is a fin_num).
 Proof. by rewrite fin_numElt; exact: idP. Qed.
@@ -1345,7 +1350,7 @@ move=> i ir; apply/implyP => Pi; apply/eqP.
 have rPF : {in r, forall i, P i ==> (F i \is a fin_num)}.
   move=> j jr; apply/implyP => Pj; rewrite fin_numElt; apply/andP; split.
     by rewrite (lt_le_trans _ (F0 _ Pj))// ltNye.
-  rewrite ltNge; apply/eqP; rewrite lee_pinfty_eq; apply/eqP/negP => /eqP Fjoo.
+  rewrite ltNge; apply/eqP; rewrite leye_eq; apply/eqP/negP => /eqP Fjoo.
   have PFninfty k : P k -> F k != -oo%E.
     by move=> Pk; rewrite gt_eqF// (lt_le_trans _ (F0 _ Pk))// ltNye.
   have /esum_pinftyP : exists i, [/\ i \in r, P i & F i = +oo%E] by exists j.
@@ -1585,16 +1590,14 @@ move: a b x y => [a| |] [b| |] [x| |] [y| |]; rewrite ?(leey, leNye)//.
 by rewrite !lee_fin; exact: ler_add.
 Qed.
 
-Lemma lte_le_add a b x y : a \is a fin_num -> b \is a fin_num ->
-  a < x -> b <= y -> a + b < x + y.
+Lemma lte_le_add a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
 Proof.
-move: x y a b => [x| |] [y| |] [a| |] [b| |] _ _ //=; rewrite ?(ltey, ltNye)//.
+move: x y a b => [x| |] [y| |] [a| |] [b| |] _ //=; rewrite ?(ltey, ltNye)//.
 by rewrite !lte_fin; exact: ltr_le_add.
 Qed.
 
-Lemma lee_lt_add a b x y : a \is a fin_num -> b \is a fin_num ->
-  a <= x -> b < y -> a + b < x + y.
-Proof. by move=> afin bin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed.
+Lemma lee_lt_add a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.
+Proof. by move=> afin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed.
 
 Lemma lee_sub x y z u : x <= y -> u <= z -> x - z <= y - u.
 Proof.
@@ -2168,7 +2171,7 @@ by apply/esym/max_idPl; rewrite lee_add2l// ltW.
 Qed.
 
 Lemma maxye : left_zero (+oo : \bar R) maxe.
-Proof. by move=> x; have [|//] := leP +oo x; rewrite lee_pinfty_eq => /eqP. Qed.
+Proof. by move=> x; have [|//] := leP +oo x; rewrite leye_eq => /eqP. Qed.
 
 Lemma maxey : right_zero (+oo : \bar R) maxe.
 Proof. by move=> x; rewrite maxC maxye. Qed.
@@ -2180,7 +2183,7 @@ Lemma maxeNy : right_id (-oo : \bar R) maxe.
 Proof. by move=> x; rewrite maxC maxNye. Qed.
 
 Lemma minNye : left_zero (-oo : \bar R) mine.
-Proof. by move=> x; have [|//] := leP x -oo; rewrite lee_ninfty_eq => /eqP. Qed.
+Proof. by move=> x; have [|//] := leP x -oo; rewrite leeNy_eq => /eqP. Qed.
 
 Lemma mineNy : right_zero (-oo : \bar R) mine.
 Proof. by move=> x; rewrite minC minNye. Qed.
@@ -2307,8 +2310,8 @@ Proof.
 move: x => [x _|//|//] /[!(@lte_fin R)] x0 [y| |] [z| |].
 - by rewrite -2!EFinM 2!lee_fin ler_pmul2l.
 - by rewrite mulry gtr0_sg// mul1e 2!leey.
-- by rewrite mulrNy gtr0_sg// mul1e 2!lee_ninfty_eq.
-- by rewrite mulry gtr0_sg// mul1e 2!lee_pinfty_eq.
+- by rewrite mulrNy gtr0_sg// mul1e 2!leeNy_eq.
+- by rewrite mulry gtr0_sg// mul1e 2!leye_eq.
 - by rewrite mulry gtr0_sg// mul1e.
 - by rewrite mulry mulrNy gtr0_sg// mul1e mul1e.
 - by rewrite mulrNy gtr0_sg// mul1e 2!leNye.
@@ -2408,10 +2411,9 @@ Proof. rewrite -fin_numN !dual_addeE lte_opp -lte_opp; exact: lte_le_sub. Qed.
 Lemma lee_dsub x y z t : x <= y -> t <= z -> x - z <= y - t.
 Proof. rewrite !dual_addeE lee_oppl oppeK -lee_opp !oppeK; exact: lee_add. Qed.
 
-Lemma lte_le_dsub z u x y : z \is a fin_num -> u \is a fin_num ->
-  x < z -> u <= y -> x - y < z - u.
+Lemma lte_le_dsub z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u.
 Proof.
-rewrite -(fin_numN z) !dual_addeE lte_opp !oppeK -lte_opp; exact: lte_le_add.
+rewrite !dual_addeE lte_opp !oppeK -lte_opp; exact: lte_le_add.
 Qed.
 
 Lemma lee_dsum I (f g : I -> \bar R) s (P : pred I) :
@@ -2893,8 +2895,8 @@ Lemma ereal_ub_ninfty S : ubound S -oo -> S = set0 \/ S = [set -oo].
 Proof.
 have [->|/set0P[x Sx] Snoo] := eqVneq S set0; first by left.
 right; rewrite predeqE => y; split => [/Snoo|->{y}].
-  by rewrite lee_ninfty_eq => /eqP ->.
-by have := Snoo _ Sx; rewrite lee_ninfty_eq => /eqP <-.
+  by rewrite leeNy_eq => /eqP ->.
+by have := Snoo _ Sx; rewrite leeNy_eq => /eqP <-.
 Qed.
 
 Lemma ereal_supremums_set0_ninfty : supremums (@set0 (\bar R)) -oo.
@@ -2905,7 +2907,7 @@ Proof.
 move=> Spoo; rewrite /supremum ifF; last by apply/eqP => S0; rewrite S0 in Spoo.
 have sSoo : supremums S +oo.
   split; first exact: ereal_ub_pinfty.
-  by move=> /= y /(_ _ Spoo); rewrite lee_pinfty_eq => /eqP ->.
+  by move=> /= y /(_ _ Spoo); rewrite leye_eq => /eqP ->.
 case: xgetP.
   by move=> _ -> sSxget; move: (is_subset1_supremums sSoo sSxget).
 by move/(_ +oo) => gSoo; exfalso; apply gSoo => {gSoo}.
@@ -3062,8 +3064,7 @@ have := leNye esup; rewrite le_eqVlt => /predU1P[/esym|ooesup].
   case: A0 => i Ai.
   by move=> /ereal_sup_ninfty /(_ i%:E) /(_ (ex_intro2 A _ i Ai erefl)).
 have esup_fin_num : esup \is a fin_num.
-  rewrite fin_numE -lee_ninfty_eq -ltNge ooesup /= -lee_pinfty_eq -ltNge.
-  by rewrite esupoo.
+  by rewrite fin_numE -leeNy_eq -ltNge ooesup /= -leye_eq -ltNge esupoo.
 rewrite -(@fineK _ esup) // lee_fin leNgt.
 apply/negP => /(sup_gt A0)[r Ar]; apply/negP; rewrite -leNgt.
 by rewrite -lee_fin fineK//; apply: ereal_sup_ub; exists r.
@@ -4375,7 +4376,7 @@ case: x => /= [x [_/posnumP[d] dP] |[d [dreal dP]] |[d [dreal dP]]]; last 2 firs
 have /ZnatP [N Nfloor] : floor (d%:num^-1) \is a Znat.
   by rewrite Znat_def floor_ge0.
 exists N => // n leNn; have gt0Sn : (0 < n%:R + 1 :> R)%R.
-  apply: ltr_spaddr => //; exact/ler0n.
+  by apply: ltr_spaddr => //; exact/ler0n.
 apply: dP; last first.
   by rewrite eq_sym addrC -subr_eq subrr eq_sym; apply/invr_neq0/lt0r_neq0.
 rewrite /= opprD addrA subrr distrC subr0 gtr0_norm; last by rewrite invr_gt0.

theories/esum.v

@@ -148,7 +148,7 @@ move=> ag0 bg0; apply/eqP; rewrite eq_le; apply/andP; split.
 wlog : a b ag0 bg0 / \esum_(i in I) a i \isn't a fin_num => [saoo|]; last first.
   move=> /fin_numPn[->|/[dup] aoo ->]; first by rewrite leNye.
   rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: esum.
-  rewrite lee_pinfty_eq; apply/eqP/eq_infty => y; rewrite esum_ge//.
+  rewrite leye_eq; apply/eqP/eq_infty => y; rewrite esum_ge//.
   have : y%:E < \esum_(i in I) a i by rewrite aoo// ltey.
   move=> /ereal_sup_gt[_ [X XI] <-] /ltW yle; exists X => //=.
   rewrite (le_trans yle)// big_split lee_addl// big_seq_cond sume_ge0 => // i.
@@ -161,7 +161,7 @@ have saX : \sum_(i <- X) a i \is a fin_num.
   apply: contraTT sa => /fin_numPn[] sa.
     suff : \sum_(i <- X) a i >= 0 by rewrite sa.
     by rewrite big_seq_cond sume_ge0 => // i; rewrite ?andbT => /XI/ag0.
-  apply/fin_numPn; right; apply/eqP; rewrite -lee_pinfty_eq esum_ge//.
+  apply/fin_numPn; right; apply/eqP; rewrite -leye_eq esum_ge//.
   by exists X; rewrite // sa.
 rewrite lee_subr_addr// addeC -lee_subr_addr// ub_ereal_sup//= => _ [Y YI] <-.
 rewrite lee_subr_addr// addeC esum_ge//; exists (X `|` Y)%fset.

theories/lebesgue_integral.v

@@ -1513,7 +1513,7 @@ Lemma le_approx k x (f0 : forall x, (0 <= f x)%E) : D x ->
   ((approx k x)%:E <= f x)%E.
 Proof.
 move=> Dx; have [fixoo|] := ltP (f x) (+oo%E); last first.
-  by rewrite lee_pinfty_eq => /eqP ->; rewrite leey.
+  by rewrite leye_eq => /eqP ->; rewrite leey.
 have nd_ag : {homo approx ^~ x : n m / (n <= m)%N >-> n <= m}.
   by move=> m n mn; exact/lefP/nd_approx.
 have fi0 y : D y -> (0 <= f y)%E by move=> ?; exact: f0.
@@ -1996,7 +1996,7 @@ have := leey (g n t); rewrite le_eqVlt => /predU1P[|] fntoo.
       exact/lef_at/nd_approx.
     by move/nondecreasing_dvg_lt => /(_ h).
   have -> : lim (EFin \o max_g2 ^~ t) = +oo.
-    by have := lim_g2_max_g2 t n; rewrite g2oo lee_pinfty_eq => /eqP.
+    by have := lim_g2_max_g2 t n; rewrite g2oo leye_eq => /eqP.
   by rewrite leey.
 - have approx_g_g := @cvg_approx _ _ _ setT _ t (fun t _ => g0 n t) Logic.I fntoo.
   have <- : lim (EFin \o g2 n ^~ t) = g n t.
@@ -2122,8 +2122,7 @@ rewrite le_eqVlt => /predU1P[<-|if_gt0].
   by under eq_fun do rewrite mule0.
 rewrite gt0_mulye//; apply/cvg_lim => //; apply/ereal_cvgPpinfty => M M0.
 near=> n; have [ifoo|] := ltP (\int[mu]_(x in D) (f x)) +oo; last first.
-  rewrite lee_pinfty_eq => /eqP ->;  rewrite mulry muleC.
-  rewrite gt0_mulye ?leey//.
+  rewrite leye_eq => /eqP ->; rewrite mulry muleC gt0_mulye ?leey//.
   by near: n; exists 1%N => // n /= n0; rewrite gtr0_sg// ?lte_fin// ltr0n.
 rewrite -(@fineK _ (\int[mu]_(x in D) f x)); last first.
   by rewrite fin_numElt ifoo andbT (le_lt_trans _ if_gt0).
@@ -2187,10 +2186,10 @@ have [f_fin _|] := boolP (\int[mu]_(x in D) f^\- x \is a fin_num).
   rewrite integralE// [in RHS]integralE// oppeD ?fin_numN// oppeK addeC.
   by rewrite funenegN.
 rewrite fin_numE negb_and 2!negbK => /orP[nfoo|/eqP nfoo].
-  exfalso; move/negP : nfoo; apply; rewrite -lee_ninfty_eq; apply/negP.
+  exfalso; move/negP : nfoo; apply; rewrite -leeNy_eq; apply/negP.
   by rewrite -ltNge (lt_le_trans _ (integral_ge0 _ _)).
 rewrite nfoo adde_defEninfty.
-rewrite -lee_pinfty_eq -ltNge lte_pinfty_eq => /orP[f_fin|/eqP pfoo].
+rewrite -leye_eq -ltNge lte_pinfty_eq => /orP[f_fin|/eqP pfoo].
   rewrite integralE// [in RHS]integralE// nfoo [in RHS]addeC oppeD//.
   by rewrite funenegN.
 by rewrite integralE// [in RHS]integralE// funeposN funenegN nfoo pfoo.
@@ -2208,7 +2207,8 @@ End integralN.
 
 Section integral_cst.
 Local Open Scope ereal_scope.
-Variables (d : measure_display) (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}).
+Variables (d : measure_display) (T : measurableType d) (R : realType)
+          (mu : {measure set T -> \bar R}).
 Variables (f : T -> \bar R) (D : set T) (mD : measurable D).
 
 Lemma sintegral_cst (x : {nonneg R}) :
@@ -2247,7 +2247,7 @@ rewrite monotone_convergence //.
     by rewrite funeqE => n; rewrite -integral_cst.
   apply/cvg_lim => //; apply/ereal_cvgPpinfty => M M0.
   have [muDoo|muDoo] := ltP (mu D) +oo; last first.
-    exists 1%N => // m /= m0; move: muDoo; rewrite lee_pinfty_eq => /eqP ->.
+    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.
@@ -2978,7 +2978,7 @@ have [M M0 muM] : exists2 M, (0 <= M)%R &
 apply/eqP/negPn/negP => /eqP muED0.
 move/not_forallP : muM; apply.
 have [muEDoo|] := ltP (mu (E `&` D)) +oo; last first.
-  by rewrite lee_pinfty_eq => /eqP ->; exists 1%N; rewrite mul1e lee_pinfty_eq.
+  by rewrite leye_eq => /eqP ->; exists 1%N; rewrite mul1e leye_eq.
 exists `|ceil (M * (fine (mu (E `&` D)))^-1)|%N.+1.
 apply/negP; rewrite -ltNge.
 rewrite -[X in _ * X](@fineK _ (mu (E `&` D))); last first.

theories/lebesgue_measure.v

@@ -698,8 +698,7 @@ Qed.
 
 Lemma itv_cpinfty_pinfty : `[+oo%E, +oo[%classic = [set +oo%E] :> set (\bar R).
 Proof.
-rewrite set_itvE predeqE => t; split => /= [|<-//].
-by rewrite lee_pinfty_eq => /eqP.
+by rewrite set_itvE predeqE => t; split => /= [|<-//]; rewrite leye_eq => /eqP.
 Qed.
 
 Lemma itv_opinfty_pinfty : `]+oo%E, +oo[%classic = set0 :> set (\bar R).
@@ -1385,7 +1384,7 @@ Qed.
 Lemma measurable_set1_pinfty : G.-sigma.-measurable [set +oo].
 Proof.
 apply: sub_sigma_algebra; exists +oo; rewrite predeqE => x; split => [->//|/=].
-by rewrite in_itv /= andbT lee_pinfty_eq => /eqP ->.
+by rewrite in_itv /= andbT leye_eq => /eqP ->.
 Qed.
 
 Lemma measurableE : emeasurable (R.-ocitv.-measurable) = G.-sigma.-measurable.

theories/measure.v

@@ -2137,7 +2137,7 @@ Lemma le_measure d (R : realFieldType) (T : semiRingOfSetsType d)
   {in measurable &, {homo mu : A B / A `<=` B >-> (A <= B)%E}}.
 Proof.
 move=> A B; rewrite ?inE => mA mB AB; have [|muBfin] := leP +oo%E (mu B).
-  by rewrite lee_pinfty_eq => /eqP ->; rewrite leey.
+  by rewrite leye_eq => /eqP ->; rewrite leey.
 rewrite -[leRHS]SetRing.RmuE// -[B](setDUK AB) measureU/= ?setDIK//.
 - by rewrite SetRing.RmuE ?lee_addl.
 - exact: sub_gen_smallest.
@@ -2485,9 +2485,9 @@ Lemma eq_measureU d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
 Proof.
 move=> mA mB muA muB muAB; have [mu'ANoo|] := ltP (mu' A) +oo.
   by rewrite !measureUfinl ?muA ?muB ?muAB.
-rewrite lee_pinfty_eq => /eqP mu'A; transitivity (+oo : \bar R); apply/eqP.
-  by rewrite -lee_pinfty_eq -mu'A -muA le_measure ?inE//=; apply: measurableU.
-by rewrite eq_sym -lee_pinfty_eq -mu'A le_measure ?inE//=; apply: measurableU.
+rewrite leye_eq => /eqP mu'A; transitivity (+oo : \bar R); apply/eqP.
+  by rewrite -leye_eq -mu'A -muA le_measure ?inE//=; apply: measurableU.
+by rewrite eq_sym -leye_eq -mu'A le_measure ?inE//=; apply: measurableU.
 Qed.
 
 Lemma null_set_setU d (R : realFieldType) (T : ringOfSetsType d)
@@ -2816,7 +2816,7 @@ suff : forall n, \sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X.
   - rewrite -lee_subr_addr //; apply ub_ereal_sup => /= _ [n _] <-.
     by rewrite EFinN lee_subr_addr // -XAx XA.
   - suff : mu X = +oo by move=> ->; rewrite leey.
-    by apply/eqP; rewrite -lee_pinfty_eq -XAx le_outer_measure.
+    by apply/eqP; rewrite -leye_eq -XAx le_outer_measure.
   - by rewrite addeC /= leNye.
 move=> n.
 apply (@le_trans _ _ (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` B n))).
@@ -3331,11 +3331,11 @@ have ? : cvg (eseries (Rmu \o B)) by exact/is_cvg_nneseries.
 have [def|] := boolP (adde_def (lim BA) (lim BNA)); last first.
   rewrite /adde_def negb_and !negbK=> /orP[/andP[BAoo BNAoo]|/andP[BAoo BNAoo]].
   - suff -> : lim (eseries (Rmu \o B)) = +oo by rewrite leey.
-    apply/eqP; rewrite -lee_pinfty_eq -(eqP BAoo); apply/lee_lim => //.
+    apply/eqP; rewrite -leye_eq -(eqP BAoo); apply/lee_lim => //.
     near=> n; apply: lee_sum => m _; apply: le_measure; rewrite /mkset; by
       [rewrite inE; exact: measurableI | rewrite inE | apply: subIset; left].
   - suff -> : lim (eseries (Rmu \o B)) = +oo by rewrite leey.
-    apply/eqP; rewrite -lee_pinfty_eq -(eqP BNAoo); apply/lee_lim => //.
+    apply/eqP; rewrite -leye_eq -(eqP BNAoo); apply/lee_lim => //.
     by near=> n; apply: lee_sum => m _; rewrite -setDE; apply: le_measure;
        rewrite /mkset ?inE//; apply: measurableD.
 rewrite -ereal_limD // (_ : (fun _ => _) =