addressing comments

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -117,7 +117,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`
 
@@ -157,6 +157,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 `charge.v`:
@@ -210,6 +216,11 @@
       `bounded_variationN`, `bounded_variationl`, `bounded_variationr`,
       `variations_opp`, `nondecreasing_bounded_variation`
 
+- 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 `probability.v`:

classical/functions.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint rat.
 From HB Require Import structures.
 From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
@@ -2700,6 +2700,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.

classical/unstable.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2022 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect finmap ssralg ssrnum ssrint.
 From mathcomp Require Import archimedean interval mathcomp_extra.
 

reals/constructive_ereal.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.              *)
 (* -------------------------------------------------------------------- *)
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)

theories/charge.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 ssralg ssrnum ssrint interval.
 From mathcomp Require Import finmap fingroup perm rat.
@@ -2174,7 +2174,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)).
@@ -2186,7 +2186,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

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 (* -------------------------------------------------------------------- *)
 (* Copyright (c) - 2015--2016 - IMDEA Software Institute                *)
 (* Copyright (c) - 2015--2018 - Inria                                   *)
@@ -58,11 +58,16 @@ Import numFieldTopology.Exports.
 From mathcomp Require Import mathcomp_extra unstable.
 
 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

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
 From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
 From mathcomp Require Import cardinality fsbigop reals ereal interval_inference.
@@ -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 *)
@@ -946,9 +948,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.
@@ -1003,7 +1003,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

@@ -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 ssralg ssrnum ssrint interval finmap.
 From mathcomp Require Import archimedean.
@@ -207,10 +207,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.
@@ -223,7 +222,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^\-.
@@ -233,17 +232,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.
@@ -268,7 +266,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 :
@@ -280,7 +278,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 :
@@ -593,8 +591,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.
@@ -741,7 +739,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.
@@ -799,7 +797,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.
@@ -813,7 +811,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.
@@ -859,7 +857,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.
@@ -908,7 +906,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 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).