Merge pull request #1664 from affeldt-aist/fixes_1616

fixes #1652

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -99,6 +99,9 @@
 - in `lebesgue_integral_fubini.v`:
   + lemmas `integral21_prod_meas2`, `integral12_prod_meas2`
 
+- in `lebesgue_integral_nonneg.v`:
+  + lemma `ge0_integral_ereal_sup` (was a `Let`)
+
 ### Changed
 
 - in `convex.v`:
@@ -257,6 +260,12 @@
   + `limZr` -> `limZl_tmp`
   + `continuousZr` -> `continuousZl_tmp`
   + `continuousZl` -> `continuousZr_tmp`
+- in `realfun.v`:
+  + `variationD` -> `variation_cat`
+
+- in `lebesgue_integrable.v`:
+  + `integral_fune_lt_pinfty` -> `integrable_lty`
+  + `integral_fune_fin_num` -> `integrable_fin_num`
 
 ### Generalized
 
@@ -294,6 +303,22 @@
   + definition `almost_everywhere_notation`
   + lemma `ess_sup_ge0`
 
+- in `exp.v`:
+  + notation `expRMm` (deprecated since 1.1.0)
+
+- in `constructive_ereal.v`:
+  + notations `lee_addl`, `lee_addr`, `lee_add2l`, `lee_add2r`, `lee_add`,
+    `lee_sub`, `lee_add2lE`, `lee_oppl`, `lee_oppr`, `lte_oppl`, `lte_oppr`,
+    `lte_add`, `lte_add2lE`, `lte_addl`, `lte_addr` (deprecated since 1.1.0)
+
+- in `measure.v`:
+  + notations `sub_additive`, `sigma_sub_additive`, `content_sub_additive`,
+    `ring_sigma_sub_additive`, `Content_SubSigmaAdditive_isMeasure.Build`,
+    `measure_sigma_sub_additive`, `measure_sigma_sub_additive_tail`,
+    `Measure_isSFinite_subdef.Build`, `sfinite_measure_subdef`,
+    `@SigmaFinite_isFinite.Build`, `FiniteMeasure_isSubProbability.Build`
+    (deprecated since 1.1.0)
+
 ### Infrastructure
 
 ### Misc

reals/constructive_ereal.v

@@ -2859,36 +2859,6 @@ Arguments lee_sum_nneg_natl {R}.
 Arguments lee_sum_npos_natl {R}.
 #[global] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply: abse_ge0] : core.
 
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDl instead.")]
-Notation lee_addl := leeDl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDr instead.")]
-Notation lee_addr := leeDr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD2l instead.")]
-Notation lee_add2l := leeD2l (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD2r instead.")]
-Notation lee_add2r := leeD2r (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD instead.")]
-Notation lee_add := leeD (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeB instead.")]
-Notation lee_sub := leeB (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD2lE instead.")]
-Notation lee_add2lE := leeD2lE (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeNl instead.")]
-Notation lee_oppl := leeNl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeNr instead.")]
-Notation lee_oppr := leeNr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteNl instead.")]
-Notation lte_oppl := lteNl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteNr instead.")]
-Notation lte_oppr := lteNr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteD instead.")]
-Notation lte_add := lteD (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteD2lE instead.")]
-Notation lte_add2lE := lteD2lE (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteDl instead.")]
-Notation lte_addl := lteDl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteDr instead.")]
-Notation lte_addr := lteDr (only parsing).
 #[deprecated(since="mathcomp-analysis 1.2.0", note="Use gee_pMl instead.")]
 Notation gee_pmull := gee_pMl (only parsing).
 #[deprecated(since="mathcomp-analysis 1.2.0", note="Use geeDl instead.")]

theories/charge.v

@@ -1140,7 +1140,7 @@ Let nu0 : nu set0 = 0. Proof. by rewrite /nu integral_set0. Qed.
 
 Let finnu A : measurable A -> nu A \is a fin_num.
 Proof.
-by move=> mA; apply: integral_fune_fin_num => //=; exact: integrableS intf.
+by move=> mA; apply: integrable_fin_num => //=; exact: integrableS intf.
 Qed.
 
 Let snu : semi_sigma_additive nu.
@@ -1151,10 +1151,10 @@ rewrite (_ : SF = fun n =>
     \sum_(0 <= i < n) (\int[mu]_(x in F i) f^\- x)); last first.
   apply/funext => n; rewrite /SF; under eq_bigr do rewrite /nu integralE.
   rewrite big_split/= sumeN//= => i j _ _.
-  rewrite fin_num_adde_defl// integral_fune_fin_num//= integrable_funeneg//=.
+  rewrite fin_num_adde_defl// integrable_fin_num//= integrable_funeneg//=.
   exact: integrableS intf.
 rewrite /nu integralE; apply: cvgeD.
-- rewrite fin_num_adde_defr// integral_fune_fin_num//=.
+- rewrite fin_num_adde_defr// integrable_fin_num//=.
   by apply: integrable_funepos => //=; exact: integrableS intf.
 - apply/semi_sigma_additive_nng_induced => //.
   by apply: measurable_funepos; exact: (measurable_int mu).

theories/exp.v

@@ -1,4 +1,4 @@
-(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
+(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum matrix.
 From mathcomp Require Import interval rat.
 From mathcomp Require Import boolp classical_sets functions mathcomp_extra.
@@ -605,9 +605,6 @@ Canonical expR_inum (i : Itv.t) (x : Itv.def (@Itv.num_sem R) i) :=
 
 End expR.
 
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `expRM_natl`")]
-Notation expRMm := expRM_natl (only parsing).
-
 Section expeR.
 Context {R : realType}.
 Implicit Types (x y : \bar R) (r s : R).

theories/ftc.v

@@ -116,7 +116,7 @@ apply: cvg_at_right_left_dnbhs.
     - rewrite addeAC -[X in _ - X]integral_itv_bndo_bndc//=; last first.
         by case: locf => + _ _; exact: measurable_funS.
       rewrite subee ?add0e//.
-      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+      by apply: integrable_fin_num => //; exact: integrableS intf.
     - by case: locf => + _ _; exact: measurable_funS.
     - apply/disj_setPRL => z/=.
       rewrite /E /= !in_itv/= => /andP[xz zxdn].
@@ -130,8 +130,8 @@ apply: cvg_at_right_left_dnbhs.
       fun n => (d n)^-1 *: fine (\int[mu]_(t in E x n) (f t)%:E)); last first.
     apply/funext => n; congr (_ *: _); rewrite -fineB/=.
     by rewrite /= (addrC (d n) x) ixdf.
-    by apply: integral_fune_fin_num => //; exact: integrableS intf.
-    by apply: integral_fune_fin_num => //; exact: integrableS intf.
+    by apply: integrable_fin_num => //; exact: integrableS intf.
+    by apply: integrable_fin_num => //; exact: integrableS intf.
   have := nice_lebesgue_differentiation nice_E locf fx.
   rewrite {ixdf} -/mu.
   rewrite [g in g n @[n --> _] --> _ -> _](_ : _ =
@@ -143,7 +143,7 @@ apply: cvg_at_right_left_dnbhs.
   suff : g = h by move=> <-.
   apply/funext => n.
   rewrite /g /h /= fineM//.
-  apply: integral_fune_fin_num => //; first exact: (nice_E _).1.
+  apply: integrable_fin_num => //; first exact: (nice_E _).1.
   by apply: integrableS intf => //; exact: (nice_E _).1.
 - apply/cvg_at_leftP => d [d_gt0 d0].
   have {}Nd_gt0 n : (0 < - d n)%R by rewrite ltrNr oppr0.
@@ -173,7 +173,7 @@ apply: cvg_at_right_left_dnbhs.
       rewrite -/mu -[LHS]oppeK; congr oppe.
       rewrite oppeB; last first.
         rewrite fin_num_adde_defl// fin_numN//.
-        by apply: integral_fune_fin_num => //; exact: integrableS intf.
+        by apply: integrable_fin_num => //; exact: integrableS intf.
       rewrite addeC.
       rewrite (_ : `]-oo, x] = `]-oo, (x + d n)%R] `|` E x n)%classic; last first.
         by rewrite -itv_bndbnd_setU//= bnd_simp ler_wnDr// ltW.
@@ -182,7 +182,7 @@ apply: cvg_at_right_left_dnbhs.
         rewrite -[X in X - _]integral_itv_bndo_bndc//; last first.
           by case: locf => + _ _; exact: measurable_funS.
         rewrite subee ?add0e//.
-        by apply: integral_fune_fin_num => //; exact: integrableS intf.
+        by apply: integrable_fin_num => //; exact: integrableS intf.
       - exact: (nice_E _).1.
       - by case: locf => + _ _; exact: measurable_funS.
       - apply/disj_setPLR => z/=.
@@ -198,7 +198,7 @@ apply: cvg_at_right_left_dnbhs.
     rewrite -/mu -[LHS]oppeK; congr oppe.
     rewrite oppeB; last first.
       rewrite fin_num_adde_defl// fin_numN//.
-      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+      by apply: integrable_fin_num => //; exact: integrableS intf.
     rewrite addeC.
     rewrite (@itv_bndbnd_setU _ _ _ (BRight (x - - d n)%R))//; last 2 first.
       case: b in ax * => /=; rewrite bnd_simp.
@@ -211,7 +211,7 @@ apply: cvg_at_right_left_dnbhs.
     - rewrite addeAC -[X in X - _]integral_itv_bndo_bndc//; last first.
         by case: locf => + _ _; exact: measurable_funS.
       rewrite opprK subee ?add0e//.
-      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+      by apply: integrable_fin_num => //; exact: integrableS intf.
     - by case: locf => + _ _; exact: measurable_funS.
     - apply/disj_setPLR => z/=.
       rewrite /E /= !in_itv/= => /andP[az zxdn].
@@ -220,16 +220,16 @@ apply: cvg_at_right_left_dnbhs.
           @[n --> \oo] --> f x.
     apply: cvg_trans; apply: near_eq_cvg; near=> n;  congr (_ *: _).
     rewrite /F -fineN -fineB; last 2 first.
-      by apply: integral_fune_fin_num => //; exact: integrableS intf.
-      by apply: integral_fune_fin_num => //; exact: integrableS intf.
+      by apply: integrable_fin_num => //; exact: integrableS intf.
+      by apply: integrable_fin_num => //; exact: integrableS intf.
     by congr fine => /=; apply/esym; rewrite (addrC _ x); near: n.
   have := nice_lebesgue_differentiation nice_E locf fx.
   rewrite {ixdf} -/mu.
   move/fine_cvgP => [_ /=].
   set g := _ \o _ => gf.
   rewrite (@eq_cvg _ _ _ _ g)// => n.
   rewrite /g /= fineM//=; last first.
-    apply: integral_fune_fin_num => //; first exact: (nice_E _).1.
+    apply: integrable_fin_num => //; first exact: (nice_E _).1.
     by apply: integrableS intf => //; exact: (nice_E _).1.
     by rewrite muE inver oppr_eq0 lt_eqF.
   by rewrite muE/= inver oppr_eq0 lt_eqF// invrN mulNr -mulrN.
@@ -377,7 +377,7 @@ have acbc : `[a, c] `<=` `[a, b].
   apply: subset_itvl; rewrite bnd_simp; move: ac; near: c.
   exact: lt_nbhsl_le.
 rewrite -lee_fin fineK; last first.
-  apply: integral_fune_fin_num => //=.
+  apply: integrable_fin_num => //=.
   rewrite (_ : (fun _ => _) = abse \o ((EFin \o f) \_ `[a, b])); last first.
     by apply/funext => x /=; rewrite restrict_EFin.
   apply/integrable_abse/integrable_restrict => //=.
@@ -641,7 +641,7 @@ have GbFbc : G b = (F b - c)%R.
 rewrite -EFinB -cE -GbFbc /G /Rintegral/= fineK//.
   rewrite integralEpatch//=.
   by under eq_integral do rewrite restrict_EFin.
-exact: integral_fune_fin_num.
+exact: integrable_fin_num.
 Unshelve. all: by end_near. Qed.
 
 Lemma ge0_continuous_FTC2y (f F : R -> R) a (l : R) :
@@ -826,7 +826,7 @@ have ? : mu.-integrable `[a, b] (fun x => ((f * G) x)%:E).
   + have := derivable_oo_continuous_bnd_within Gab.
     by move/subspace_continuousP; exact.
 rewrite /= integralD//=.
-- by rewrite addeAC subee ?add0e// integral_fune_fin_num.
+- by rewrite addeAC subee ?add0e// integrable_fin_num.
 - apply: continuous_compact_integrable => //; first exact: segment_compact.
   apply/subspace_continuousP => x abx;apply: cvgM.
   + have := derivable_oo_continuous_bnd_within Fab.

theories/gauss_integral.v

@@ -262,7 +262,7 @@ under eq_integral do rewrite fctE/= EFinM.
 have ? : mu.-integrable `[0, 1] (fun y => (gauss_fun (y * x))%:E).
   apply: continuous_compact_integrable => //; first exact: segment_compact.
   by apply: continuous_subspaceT => z; exact: continuous_gaussM.
-rewrite integralZr//= fineM//=; last exact: integral_fune_fin_num.
+rewrite integralZr//= fineM//=; last exact: integrable_fin_num.
 by rewrite mulrC.
 Qed.
 
@@ -288,10 +288,10 @@ have -> : gauss_fun x = \int[mu]_(t in `[0, 1]) cst (gauss_fun x) t.
   rewrite Rintegral_cst//.
   by rewrite /mu/= lebesgue_measure_itv//= lte01 oppr0 addr0 mulr1.
 rewrite fine_le//.
-- apply: integral_fune_fin_num => //=.
+- apply: integrable_fin_num => //=.
   apply: continuous_compact_integrable; first exact: segment_compact.
   by apply: continuous_in_subspaceT => z _; exact: continuous_u.
-- apply: integral_fune_fin_num => //=.
+- apply: integrable_fin_num => //=.
   apply: continuous_compact_integrable; first exact: segment_compact.
   by apply: continuous_subspaceT => z; exact: cvg_cst.
 apply: ge0_le_integral => //=.

theories/lebesgue_integral_theory/lebesgue_Rintegral.v

@@ -92,7 +92,7 @@ Lemma RintegralZl D f r : measurable D -> mu.-integrable D (EFin \o f) ->
   \int[mu]_(x in D) (r * f x) = r * \int[mu]_(x in D) f x.
 Proof.
 move=> mD intf; rewrite (_ : r = fine r%:E)// -fineM//; last first.
-  exact: integral_fune_fin_num.
+  exact: integrable_fin_num.
 by congr fine; under eq_integral do rewrite EFinM; exact: integralZl.
 Qed.
 
@@ -177,7 +177,7 @@ Lemma RintegralD D f1 f2 : measurable D ->
   \int[mu]_(x in D) f1 x + \int[mu]_(x in D) f2 x.
 Proof.
 move=> mD if1 if2.
-by rewrite /Rintegral integralD_EFin// fineD//; exact: integral_fune_fin_num.
+by rewrite /Rintegral integralD_EFin// fineD//; exact: integrable_fin_num.
 Qed.
 
 Lemma RintegralB D f1 f2 : measurable D ->
@@ -186,7 +186,7 @@ Lemma RintegralB D f1 f2 : measurable D ->
   \int[mu]_(x in D) f1 x - \int[mu]_(x in D) f2 x.
 Proof.
 move=> mD if1 if2.
-by rewrite /Rintegral integralB_EFin// fineB//; exact: integral_fune_fin_num.
+by rewrite /Rintegral integralB_EFin// fineB//; exact: integrable_fin_num.
 Qed.
 
 End Rintegral.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -720,12 +720,12 @@ Qed.
 
 End integralB.
 
-Section integrable_fune.
+Section integrable_lty_fin_num.
 Context d (T : measurableType d) (R : realType).
 Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
 Local Open Scope ereal_scope.
 
-Lemma integral_fune_lt_pinfty (f : T -> \bar R) :
+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//;
@@ -734,15 +734,19 @@ rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lteNl ltNye_eq.
 by rewrite integrable_neg_fin_num.
 Qed.
 
-Lemma integral_fune_fin_num (f : T -> \bar R) :
+Lemma integrable_fin_num (f : T -> \bar R) :
   mu.-integrable D f -> \int[mu]_(x in D) f x \is a fin_num.
 Proof.
-move=> h; apply/fin_numPlt; rewrite integral_fune_lt_pinfty// andbC/= -/(- +oo).
-rewrite lteNl -integralN; first exact/integral_fune_lt_pinfty/integrableN.
+move=> h; apply/fin_numPlt; rewrite integrable_lty// andbC/= -/(- +oo).
+rewrite lteNl -integralN; first exact/integrable_lty/integrableN.
 by rewrite fin_num_adde_defl// fin_numN integrable_neg_fin_num.
 Qed.
 
-End integrable_fune.
+End integrable_lty_fin_num.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `integrable_lty`")]
+Notation integral_fune_lt_pinfty := integrable_lty (only parsing).
+#[deprecated(since="mathcomp-analysis 1.12.0", note="renamed to `integrable_fin_num`")]
+Notation integral_fune_fin_num := integrable_fin_num (only parsing).
 
 Section transfer.
 Context d1 d2 (X : measurableType d1) (Y : measurableType d2) (R : realType).

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -115,7 +115,7 @@ have [g [gfe2 ig]] : exists g : {sfun R >-> rT},
   have [g_ [intG ?]] := approximation_sfun_integrable mE intf.
   move/fine_fcvg/cvg_ballP/(_ (eps%:num / 2)%R) => -[] // n _ Nb; exists (g_ n).
   have fg_fin_num : \int[mu]_(z in E) `|(f z - g_ n z)%:E| \is a fin_num.
-    rewrite integral_fune_fin_num// integrable_abse//.
+    rewrite integrable_fin_num// integrable_abse//.
     by under eq_fun do rewrite EFinB; apply: integrableB => //; exact: intG.
   split; last exact: intG.
   have /= := Nb _ (leqnn n); rewrite /ball/= sub0r normrN -fine_abse// -lte_fin.
@@ -228,9 +228,9 @@ have -> : f x = (r *+ 2)^-1 * \int[mu]_(z in `[x - r, x + r]) cst (f x) z.
 have intRf : mu.-integrable `[x - r, x + r] (EFin \o f).
   exact: (@integrableS _ _ _ mu _ _ _ _ _ xrA intf).
 rewrite /= -mulrBr -fineB; first last.
-- rewrite integral_fune_fin_num// continuous_compact_integrable// => ?.
+- rewrite integrable_fin_num// continuous_compact_integrable// => ?.
   exact: cvg_cst.
-- by rewrite integral_fune_fin_num.
+- by rewrite integrable_fin_num.
 rewrite -integralB_EFin //; first last.
   by apply: continuous_compact_integrable => // ?; exact: cvg_cst.
 under [fun _ => _ + _ ]eq_fun => ? do rewrite -EFinD.
@@ -239,17 +239,17 @@ have int_fx : mu.-integrable `[x - r, x + r] (fun z => (f z - f x)%:E).
   rewrite integrableB// continuous_compact_integrable// => ?.
   exact: cvg_cst.
 rewrite normrM ger0_norm // -fine_abse //; first last.
-  by rewrite integral_fune_fin_num.
+  by rewrite integrable_fin_num.
 suff : (\int[mu]_(z in `[(x - r)%R, (x + r)%R]) `|f z - f x|%:E <=
     (r *+ 2 * eps)%:E)%E.
   move=> intfeps; apply: le_trans.
     apply: (ler_pM r20 _ (le_refl _)); first exact: fine_ge0.
     apply: fine_le; last apply: le_abse_integral => //.
-    - by rewrite abse_fin_num integral_fune_fin_num.
-    - by rewrite integral_fune_fin_num// integrable_abse.
+    - by rewrite abse_fin_num integrable_fin_num.
+    - by rewrite integrable_fin_num// integrable_abse.
     - by case/integrableP : int_fx.
   rewrite ler_pdivrMl ?mulrn_wgt0 // -[_ * _]/(fine (_%:E)).
-  by rewrite fine_le// integral_fune_fin_num// integrable_abse.
+  by rewrite fine_le// integrable_fin_num// integrable_abse.
 apply: le_trans.
 - apply: (@integral_le_bound _ _ _ _ _ (fun z => (f z - f x)%:E) eps%:E) => //.
   + by case/integrableP: int_fx.

theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v

@@ -328,8 +328,8 @@ have mfn : mu.-integrable E (fun z => `|f^\- z - (n_ n z)%:E|).
 rewrite -[X in (_ <= `|X|)%R]fineD // -integralD //.
 move: finfn finfp => _ _.
 rewrite !ger0_norm ?fine_ge0 ?integral_ge0 ?fine_le//.
-- by apply: integral_fune_fin_num => //; exact/integrable_abse/mfpn.
-- by apply: integral_fune_fin_num => //; exact: integrableD.
+- by apply: integrable_fin_num => //; exact/integrable_abse/mfpn.
+- by apply: integrable_fin_num => //; exact: integrableD.
 - apply: ge0_le_integral => //.
   + by apply: measurableT_comp => //; case/integrableP: (mfpn n).
   + by move=> x Ex; rewrite adde_ge0.