addressing comments

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -76,7 +76,7 @@
   + defintions `funrpos`, `funrneg` with notations `^\+` and `^\-`
   + lemmas `funrpos_ge0`, `funrneg_ge0`, `funrposN`, `funrnegN`, `ge0_funrposE`,
     `ge0_funrnegE`, `le0_funrposE`, `le0_funrnegE`, `ge0_funrposM`, `ge0_funrnegM`,
-    `le0_funrposM`, `le0_funrnegM`, `funr_normr`, `funrposneg`, `funrD_Dpos`,
+    `le0_funrposM`, `le0_funrnegM`, `funrposDneg`, `funrposBneg`,
     `funrD_posD`, `funrpos_le`, `funrneg_le`
   + lemmas `funerpos`, `funerneg`
 
@@ -116,6 +116,12 @@
     `ge0_independent_expectationM`, `independent_Lfun1_expectationM_lty`,
     `independent_Lfun1M`, `independent_expectationM`
 
+- in `functions.v`:
+  + lemma `addBrfctE`
+
+- in `ereal.v`:
+  + lemma `ge0_addBefctE`
+
 ### Changed
 - in set_interval.v
   + `itv_is_closed_unbounded` (fix the definition)
@@ -234,6 +240,11 @@
 - moved from `convex.v` to `realfun.v`
   + lemma `second_derivative_convex`
 
+- in `numfun.v`:
+  + `fune_abse` renamed to `funeposDneg` and direction of the equality changed
+  + `funeposneg` renamed to `funeposBneg` and direction of the equality changed
+  + `funeD_posD` renamed to `funeDB` and direction of the equality changed
+
 ### Renamed
 - in `set_interval.v`:
   + `itv_is_ray` -> `itv_is_open_unbounded`

classical/functions.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
 #[warning="-warn-library-file-internal-analysis"]
@@ -2702,6 +2702,10 @@ Proof. by elim: n => [//|n h]; rewrite funeqE=> ?; rewrite !mulrSr h. Qed.
 Lemma opprfctE (T : Type) (K : zmodType) (f : T -> K) : - f = (fun x => - f x).
 Proof. by []. Qed.
 
+Lemma addBrfctE (U : Type) (K : zmodType) :
+  @interchange (U -> K) (fun a b => a - b) (fun a b => a + b).
+Proof. by move=> a b c d; apply/funext => x; rewrite addrACA -opprD. Qed.
+
 Lemma mulrfctE (T : Type) (K : pzRingType) (f g : T -> K) :
   f * g = (fun x => f x * g x).
 Proof. by []. Qed.

theories/charge.v

@@ -2176,7 +2176,7 @@ Lemma Radon_Nikodym_change_of_variables f E : measurable E ->
   \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) =
   \int[nu]_(x in E) f x.
 Proof.
-move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first.
+move=> mE mf; rewrite -[in RHS](funeposBneg f) integralB //; last 2 first.
   - exact: integrable_funepos.
   - exact: integrable_funeneg.
 transitivity (\int[mu]_(x in E) (f x * Radon_Nikodym_SigmaFinite.f nu mu x)).
@@ -2188,7 +2188,7 @@ transitivity (\int[mu]_(x in E) (f x * Radon_Nikodym_SigmaFinite.f nu mu x)).
     exact: measurable_int (Radon_Nikodym_SigmaFinite.f_integrable _).
   - apply: ae_eqe_mul2l.
     exact/ae_eq_sym/ae_eq_Radon_Nikodym_SigmaFinite.
-rewrite [in LHS](funeposneg f).
+rewrite -[in LHS](funeposBneg f).
 under [in LHS]eq_integral => x xE. rewrite muleBl; last 2 first.
   - exact: Radon_Nikodym_SigmaFinite.f_fin_num.
   - exact: add_def_funeposneg.

theories/ereal.v

@@ -61,6 +61,13 @@ Local Open Scope ring_scope.
 Local Open Scope ereal_scope.
 Local Open Scope classical_set_scope.
 
+Lemma ge0_addBefctE (T : Type) (R : realDomainType) (a b c d : T -> \bar R) :
+  (forall x, 0 <= c x) -> (forall x, 0 <= d x) ->
+  a + b \- (c + d) = a \- c + (b \- d).
+Proof.
+by move=> ? ?; apply/funext=> x; rewrite !fctE addeACA oppeD ?ge0_adde_def ?inE.
+Qed.
+
 Lemma EFin_bigcup T (F : nat -> set T) :
   EFin @` (\bigcup_i F i) = \bigcup_i (EFin @` F i).
 Proof.

theories/esum.v

@@ -507,14 +507,14 @@ Proof. by move=> Df; rewrite summableN; exact: summableD. Qed.
 
 Lemma summable_funepos D f : summable D f -> summable D f^\+.
 Proof.
-apply: le_lt_trans; apply le_esum => t Dt.
-by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl.
+apply: le_lt_trans; apply: le_esum => t Dt.
+by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl.
 Qed.
 
 Lemma summable_funeneg D f : summable D f -> summable D f^\-.
 Proof.
-apply: le_lt_trans; apply le_esum => t Dt.
-by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDr.
+apply: le_lt_trans; apply: le_esum => t Dt.
+by rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr.
 Qed.
 
 End summable_lemmas.
@@ -596,7 +596,7 @@ have -> : (C_ = A_ \- B_)%R.
   apply/funext => k.
   rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//.
   apply eq_bigr => i Pi; rewrite -fineB//.
-  - by rewrite [in LHS](funeposneg f).
+  - by rewrite -[in LHS](funeposBneg f).
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos.
   - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funeneg.
 by rewrite distrC; apply: hN; near: n; exists N.
@@ -653,14 +653,14 @@ rewrite [X in _ == X -> _]addeC -sube_eq; last 2 first.
   - rewrite fin_num_adde_defr// ge0_esum_posneg//.
     rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
     by rewrite /= gee0_abs// f0.
-rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq; last 2 first.
-  - rewrite ge0_esum_posneg//.
-    rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
-    by rewrite /= gee0_abs// f0.
-  - rewrite fin_num_adde_defl// ge0_esum_posneg//.
-    rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di.
-    by rewrite /= gee0_abs// g0.
-by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
+rewrite -addeA addeCA eq_sym [X in _ == X -> _]addeC -sube_eq.
+- by rewrite ge0_esum_posneg// ge0_esum_posneg// => /eqP ->.
+- rewrite ge0_esum_posneg//.
+  rewrite (@eq_esum _ _ _ _ (abse \o f))// -?summableE// => i Di.
+  by rewrite /= gee0_abs// f0.
+- rewrite fin_num_adde_defl// ge0_esum_posneg//.
+  rewrite (@eq_esum _ _ _ _ (abse \o g))// -?summableE// => i Di.
+  by rewrite /= gee0_abs// g0.
 Qed.
 
 End esumB.

theories/independence.v

@@ -13,6 +13,8 @@ From mathcomp Require Import hoelder.
 (**md**************************************************************************)
 (* # Independence                                                             *)
 (*                                                                            *)
+(* The status of this file is experimental.                                   *)
+(*                                                                            *)
 (* ```                                                                        *)
 (*   independent_events I F == the events F indexed by I are independent      *)
 (*  mutual_independence I F == the set systems F indexed by I are independent *)
@@ -1022,9 +1024,7 @@ Lemma independent_expectationM (X Y : {RV P >-> R}) :
 Proof.
 move=> XY iX iY.
 transitivity ('E_P[(X^\+ - X^\-) * (Y^\+ - Y^\-)]).
-  congr ('E_P[_]).
-  apply/funext => /=t.
-  by rewrite [in LHS](funrposneg X)/= [in LHS](funrposneg Y).
+  by rewrite !funrposBneg.
 have ? : X^\-%R \in Lfun P 1.
   apply/Lfun1_integrable; rewrite -funerneg; apply/integrable_funeneg => //.
   exact/Lfun1_integrable.
@@ -1079,7 +1079,7 @@ transitivity ('E_P[X^\+ - X^\-] * 'E_P[Y^\+ - Y^\-]).
   - by rewrite -!expectationB.
   - by rewrite fin_numB// !expectation_fin_num.
   - by rewrite fin_num_adde_defr// expectation_fin_num.
-by congr *%E; congr ('E_P[_]); rewrite [RHS]funrposneg.
+by rewrite !funrposBneg.
 Qed.
 
 End product_expectation.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -209,10 +209,9 @@ Proof. by move=> fi gi; exact/(integrableD fi)/integrableN. Qed.
 Lemma integrable_add_def f : mu_int f ->
   \int[mu]_(x in D) f^\+ x +? - (\int[mu]_(x in D) f^\- x).
 Proof.
-move=> /integrableP[mf]; rewrite -[fun x => _]/(abse \o f) fune_abse => foo.
-rewrite ge0_integralD // in foo; last 2 first.
-- exact: measurable_funepos.
-- exact: measurable_funeneg.
+move=> /integrableP[mf]; rewrite -[fun x => _]/(abse \o f) -funeposDneg => foo.
+rewrite ge0_integralD // in foo; [|exact: measurable_funepos
+                                  |exact: measurable_funeneg].
 apply: ltpinfty_adde_def.
 - by apply: le_lt_trans foo; rewrite leeDl// integral_ge0.
 - by rewrite inE (@le_lt_trans _ _ 0)// leeNl oppe0 integral_ge0.
@@ -225,7 +224,7 @@ move=> /integrableP[Df foo]; apply/integrableP; split.
 apply: le_lt_trans foo; apply: ge0_le_integral => //.
 - by apply/measurableT_comp => //; exact: measurable_funepos.
 - exact/measurableT_comp.
-- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl.
+- by move=> t Dt; rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDl.
 Qed.
 
 Lemma integrable_funeneg f : mu_int f -> mu_int f^\-.
@@ -235,17 +234,16 @@ move=> /integrableP[Df foo]; apply/integrableP; split.
 apply: le_lt_trans foo; apply: ge0_le_integral => //.
 - by apply/measurableT_comp => //; exact: measurable_funeneg.
 - exact/measurableT_comp.
-- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDr.
+- by move=> t Dt; rewrite -/((abse \o f) t) -funeposDneg gee0_abs// leeDr.
 Qed.
 
 Lemma integral_funeneg_lt_pinfty f : mu_int f -> \int[mu]_(x in D) f^\- x < +oo.
 Proof.
 move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact: measurable_funeneg.
 - exact: measurableT_comp.
-- move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0.
-    rewrite lee0_abs// funenegE.
-    by move: fx0; rewrite -{1}oppe0 -leeNr => /max_idPl ->.
+- move=> x Dx; have /orP[fx0|fx0] := le_total (f x) 0.
+    by rewrite lee0_abs// funenegE ge_max lexx leeNr oppe0 fx0.
   rewrite gee0_abs// funenegE.
   by move: (fx0); rewrite -{1}oppe0 -leeNl => /max_idPr ->.
 Qed.
@@ -270,7 +268,7 @@ rewrite fin_numElt; apply/andP; split.
 case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact/measurable_funeneg.
 - exact/measurableT_comp.
-- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDr.
+- by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDr.
 Qed.
 
 Lemma integrable_pos_fin_num f :
@@ -282,7 +280,7 @@ rewrite fin_numElt; apply/andP; split.
 case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact/measurable_funepos.
 - exact/measurableT_comp.
-- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDl.
+- by move=> x Dx; rewrite -/((abse \o f) x) -funeposDneg leeDl.
 Qed.
 
 Lemma integrableMr (h : T -> R) g :
@@ -595,8 +593,8 @@ have : (g1 \+ g2)^\+ \+ g1^\- \+ g2^\- = (g1 \+ g2)^\- \+ g1^\+ \+ g2^\+.
     by rewrite !funeposE -!fine_max.
     by rewrite funeposE !funenegE -!fine_max.
   apply/eqP.
-  rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) -funeD_posD.
-  by rewrite -[RHS]/((_ \- _) x) -funeD_Dpos.
+  rewrite -[LHS]/((g1^\+ \+ g2^\+ \- (g1^\- \+ g2^\-)) x) funeDB.
+  by rewrite -[RHS]/((_ \- _) x) funeposBneg.
 move/(congr1 (fun y => \int[mu]_(x in D) (y x) )).
 rewrite (ge0_integralD mu mD); last 4 first.
   - by move=> x _; rewrite adde_ge0.
@@ -743,7 +741,7 @@ Local Open Scope ereal_scope.
 Lemma integrable_lty (f : T -> \bar R) :
   mu.-integrable D f -> \int[mu]_(x in D) f x < +oo.
 Proof.
-move=> intf; rewrite (funeposneg f) integralB//;
+move=> intf; rewrite -(funeposBneg f) integralB//;
   [|exact: integrable_funepos|exact: integrable_funeneg].
 rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lteNl ltNye_eq.
 by rewrite integrable_neg_fin_num.
@@ -801,7 +799,7 @@ rewrite -[X in _ = _ - X]ge0_integral_pushforward//; last first.
 rewrite -integralB//=; last first.
 - by apply: integrable_funeneg => //=; exact: integrable_pushforward.
 - by apply: integrable_funepos => //=; exact: integrable_pushforward.
-- by apply/eq_integral=> // x _; rewrite /= [in LHS](funeposneg f).
+- by apply/eq_integral=> // x _; rewrite -[in LHS](funeposBneg f).
 Qed.
 
 End transfer.
@@ -815,7 +813,7 @@ Lemma negligible_integral (D N : set T) (f : T -> \bar R) :
   measurable N -> measurable D -> mu.-integrable D f ->
   mu N = 0 -> \int[mu]_(x in D) f x = \int[mu]_(x in D `\` N) f x.
 Proof.
-move=> mN mD mf muN0; rewrite [f]funeposneg ?integralB //; first last.
+move=> mN mD mf muN0; rewrite -[f]funeposBneg ?integralB//; first last.
 - exact: integrable_funeneg.
 - exact: integrable_funepos.
 - apply: (integrableS mD) => //; first exact: measurableD.
@@ -861,7 +859,7 @@ Lemma integral_measure_add : \int[measure_add m1 m2]_(x in D) f x =
 Proof.
 transitivity (\int[m1]_(x in D) (f^\+ \- f^\-) x +
               \int[m2]_(x in D) (f^\+ \- f^\-) x); last first.
-  by congr +%E; apply: eq_integral => x _; rewrite [in RHS](funeposneg f).
+  by congr +%E; apply: eq_integral => x _; rewrite -[in RHS](funeposBneg f).
 rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg].
 rewrite integralB//; [|exact: integrable_funepos|exact: integrable_funeneg].
 rewrite addeACA -ge0_integral_measure_add//; last first.
@@ -910,7 +908,7 @@ have ? : \int[mu]_(x in \bigcup_i F i) g x \is a fin_num.
 transitivity (\int[mu]_(x in \bigcup_i F i) g^\+ x -
               \int[mu]_(x in \bigcup_i F i) g^\- x)%E.
   rewrite -integralB.
-  - by apply: eq_integral => t Ft; rewrite [in LHS](funeposneg g).
+  - by apply: eq_integral => t Ft; rewrite -[in LHS](funeposBneg g).
   - exact: bigcupT_measurable.
   - by apply: integrable_funepos => //; exact: bigcupT_measurable.
   - by apply: integrable_funeneg => //; exact: bigcupT_measurable.

theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import archimedean.
@@ -297,11 +297,11 @@ exists (fun n => p_ n - n_ n)%R; split.
 - move=> n; rewrite /comp; under eq_fun => ? do rewrite sfunB /= EFinB.
   by apply: integrableB => //; [exact: intp | exact: intn].
 - move=> ? ?; rewrite /comp; under eq_fun => ? do rewrite sfunB /= EFinB.
-  rewrite [f]funeposneg; apply: cvgeB => //;[|exact: pf|exact:nf].
+  rewrite -[f]funeposBneg; apply: cvgeB => //;[|exact: pf|exact:nf].
   exact: add_def_funeposneg.
 have fpn z n : f z - ((p_ n - n_ n) z)%:E =
     (f^\+ z - (p_ n z)%:E) - (f^\- z - (n_ n z)%:E).
-  rewrite sfunB EFinB fin_num_oppeB // {1}[f]funeposneg -addeACA.
+  rewrite sfunB EFinB fin_num_oppeB // -{1}[f]funeposBneg -addeACA.
   by congr (_ _); rewrite fin_num_oppeB.
 case/integrableP: (intf) => mf _.
 have mfpn n : mu.-integrable E (fun z => f z - ((p_ n - n_ n) z)%:E).

theories/lebesgue_integral_theory/lebesgue_integral_fubini.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import archimedean.
@@ -922,7 +922,7 @@ apply: ge0_le_integral; [by []|by []|..].
   + apply: measurableT_comp => //.
     by apply: measurableT_comp => //; exact: measurable_funepos.
   + by apply: measurableT_comp => //; exact/measurableT_comp.
-  + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
+  + by move=> y _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDl.
 Qed.
 
 Let integrable_Fminus : m1.-integrable setT Fminus.
@@ -939,7 +939,7 @@ apply: ge0_le_integral; [by []|by []|..].
   + apply: measurableT_comp => //; apply: measurableT_comp => //.
     exact: measurable_funeneg.
   + by apply: measurableT_comp => //; exact: measurableT_comp.
-  + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr.
+  + by move=> y _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDr.
 Qed.
 
 Lemma integrable_fubini_F : m1.-integrable setT F.
@@ -982,7 +982,7 @@ apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..].
   + apply: measurableT_comp => //.
     by apply: measurableT_comp => //; exact: measurable_funepos.
   + by apply: measurableT_comp => //; exact: measurableT_comp.
-  + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
+  + by move=> x _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDl.
 Qed.
 
 Let integrable_Gminus : m2.-integrable setT Gminus.
@@ -997,7 +997,7 @@ apply: ge0_le_integral; [by []|by []|exact: measurableT_comp|..].
   + apply: measurableT_comp => //.
     by apply: measurableT_comp => //; exact: measurable_funeneg.
   + by apply: measurableT_comp => //; exact: measurableT_comp.
-  + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr.
+  + by move=> x _; rewrite gee0_abs// -/((abse \o f) _) -funeposDneg leeDr.
 Qed.
 
 Lemma integral12_prod_meas1 : \int[m1]_x F x = \int[m1 \x m2]_z f z.

theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v

@@ -634,16 +634,16 @@ Proof.
 have [/[!inE] aD|aD] := boolP (a \in D).
   rewrite integralE ge0_integral_dirac//; last exact/measurable_funepos.
   rewrite ge0_integral_dirac//; last exact/measurable_funeneg.
-  by rewrite [in RHS](funeposneg f) diracE mem_set// mul1e.
+  by rewrite -[in RHS](funeposBneg f) diracE mem_set// mul1e.
 rewrite diracE (negbTE aD) mul0e -(integral_measure_zero D f)//.
 apply: eq_measure_integral => //= S mS DS; rewrite /dirac indicE memNset//.
 by move=> /DS/mem_set; exact/negP.
 Qed.
 
 End integral_dirac.
 
-Lemma summable_integral_dirac {R : realType} (a : nat -> \bar R) : summable setT a ->
-  (\sum_(n <oo) `|\int[\d_ n]_x a x| < +oo)%E.
+Lemma summable_integral_dirac {R : realType} (a : (\bar R)^nat) :
+  summable setT a -> (\sum_(n <oo) `|\int[\d_ n]_x a x| < +oo)%E.
 Proof.
 move=> sa.
 apply: (@le_lt_trans _ _ (\sum_(i <oo) `|fine (a i)|%:E))%E.
@@ -747,7 +747,8 @@ transitivity (limn (fun n =>
     \int[measure_add (msum m_ N) (m_ N)]_(x in D) (f_ n x)%:E)).
   rewrite -monotone_convergence//; last first.
     by move=> t Dt a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
-  by apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
+  apply: eq_integral => t /[!inE] Dt; apply/esym/cvg_lim => //.
+  exact: cvg_nnsfun_approx.
 transitivity (limn (fun n =>
   \int[msum m_ N]_(x in D) (f_ n x)%:E + \int[m_ N]_(x in D) (f_ n x)%:E)).
   by congr (limn _); apply/funext => n; by rewrite integral_measure_add_nnsfun.
@@ -1146,14 +1147,14 @@ End ge0_cvgn_integral.
 Lemma le_abse_integral d (T : measurableType d) (R : realType)
   (mu : {measure set T -> \bar R}) (D : set T) (f : T -> \bar R)
   (mD : measurable D) : measurable_fun D f ->
-  (`| \int[mu]_(x in D) (f x) | <= \int[mu]_(x in D) `|f x|)%E.
+  (`| \int[mu]_(x in D) f x | <= \int[mu]_(x in D) `|f x|)%E.
 Proof.
 move=> mf.
 rewrite integralE (le_trans (lee_abs_sub _ _))// gee0_abs; last first.
   exact: integral_ge0.
 rewrite gee0_abs; last exact: integral_ge0.
-by rewrite -ge0_integralD // -?fune_abse//;
-  [exact: measurable_funepos | exact: measurable_funeneg].
+rewrite -ge0_integralD//; [|exact: measurable_funepos|exact: measurable_funeneg].
+by under [in leRHS]eq_integral do rewrite -/((abse \o f) _) -funeposDneg.
 Qed.
 
 Lemma abse_integralP d (T : measurableType d) (R : realType)
@@ -1163,7 +1164,7 @@ Lemma abse_integralP d (T : measurableType d) (R : realType)
 Proof.
 move=> mD mf; split => [|] foo; last first.
   exact: (le_lt_trans (le_abse_integral mu mD mf) foo).
-under eq_integral do rewrite -/((abse \o f) _) fune_abse.
+under eq_integral do rewrite -/((abse \o f) _) -funeposDneg.
 rewrite ge0_integralD//;[|exact/measurable_funepos|exact/measurable_funeneg].
 move: foo; rewrite integralE/= -fin_num_abs fin_numB => /andP[fpoo fnoo].
 by rewrite lte_add_pinfty// ltey_eq ?fpoo ?fnoo.