diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4092f4f4a8..bb6f83da8d 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/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
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 1be00e5512..5f8b5d4a76 100644
--- a/reals/constructive_ereal.v
+++ b/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.")]
diff --git a/theories/charge.v b/theories/charge.v
index 47bd0cf643..aedd8f8e14 100644
--- a/theories/charge.v
+++ b/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).
diff --git a/theories/exp.v b/theories/exp.v
index ba7fec0374..f24e01a2eb 100644
--- a/theories/exp.v
+++ b/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).
diff --git a/theories/ftc.v b/theories/ftc.v
index 9cd8670664..89676f684a 100644
--- a/theories/ftc.v
+++ b/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,8 +220,8 @@ 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.
@@ -229,7 +229,7 @@ apply: cvg_at_right_left_dnbhs.
   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.
diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v
index e3caf20ad7..5efc93ec78 100644
--- a/theories/gauss_integral.v
+++ b/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 => //=.
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index 4c635bc688..9808470294 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/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.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v
index 6a1f9626c6..a3b8f851d4 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integrable.v
+++ b/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).
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
index 420dbf497c..dea7f52d2b 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
+++ b/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.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
index e093742fbb..4efad18f7f 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
+++ b/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.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
index 67da0fcd7b..65dabf3217 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
@@ -1047,7 +1047,7 @@ Variable f : R -> R.
 Hypothesis f0 : (forall x, 0 <= f x)%R.
 Hypothesis mf : measurable_fun setT f.
 
-Let ge0_integral_ereal_sup :
+Lemma ge0_integral_ereal_sup :
   \int[mu]_(x in `[0%R, +oo[) (f x)%:E =
   ereal_sup [set \int[mu]_(x in `[0%R, i.+1%:R]) (f x)%:E | i in [set: nat]].
 Proof.
diff --git a/theories/measure.v b/theories/measure.v
index d44fafbb6f..2956ce6a65 100644
--- a/theories/measure.v
+++ b/theories/measure.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 HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean finmap.
 From mathcomp Require Import mathcomp_extra unstable boolp classical_sets.
@@ -1906,10 +1906,6 @@ move=> /(amx (bigcup2 A B))->.
 Qed.
 
 End additivity.
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `subadditive`")]
-Notation sub_additive := subadditive (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `measurable_subset_sigma_subadditive`")]
-Notation sigma_sub_additive := measurable_subset_sigma_subadditive (only parsing).
 
 Section ring_additivity.
 Context d (R : numFieldType) (T : ringOfSetsType d) (mu : set T -> \bar R).
@@ -3016,8 +3012,6 @@ Qed.
 (* Qed. *)
 
 End more_content_semiring_lemmas.
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `content_sub_additive`")]
-Notation content_sub_additive := content_subadditive (only parsing).
 
 Section content_ring_lemmas.
 Context d (R : realType) (T : ringOfSetsType d).
@@ -3119,8 +3113,6 @@ by under eq_fun do under eq_bigr do rewrite SetRing.RmuE//=.
 Qed.
 
 End ring_sigma_subadditive_content.
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `ring_sigma_subadditive`")]
-Notation ring_sigma_sub_additive := ring_sigma_subadditive (only parsing).
 
 #[key="mu"]
 HB.factory Record Content_SigmaSubAdditive_isMeasure d (R : realType)
@@ -3135,16 +3127,6 @@ HB.instance Definition _ := Content_isMeasure.Build d T R mu
 
 HB.end.
 
-#[deprecated(since="mathcomp-analysis 1.1.0",
-  note="renamed `Content_SigmaSubAdditive_isMeasure.Build`")]
-Notation "'Content_SubSigmaAdditive_isMeasure.Build' d R T mu" :=
-  (@Content_SigmaSubAdditive_isMeasure.Build d R T mu)
-  (at level 2, d, R, T, mu at next level, only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0",
-  note="renamed `measure_sigma_subadditive`")]
-Notation measure_sigma_sub_additive :=
-  Content_SigmaSubAdditive_isMeasure.measure_sigma_subadditive (only parsing).
-
 Section more_premeasure_ring_lemmas.
 Context d (R : realType) (T : semiRingOfSetsType d).
 Variable mu : {measure set T -> \bar R}.
@@ -3246,8 +3228,6 @@ rewrite (@eq_eseriesr _ _ (fun n => mu (if (N <= n)%N then F n else set0))).
     by under eq_bigcupr do rewrite mem_not_I.
 - by move=> o _; rewrite (fun_if mu) measure0.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `measure_sigma_subadditive_tail`")]
-Notation measure_sigma_sub_additive_tail := measure_sigma_subadditive_tail (only parsing).
 
 Section ring_sigma_content.
 Context d (R : realType) (T : semiRingOfSetsType d)
@@ -3329,11 +3309,6 @@ HB.structure Definition SFiniteMeasure d (T : sigmaRingType d) (R : realType) :=
   {mu of @Measure _ T R mu & isSFinite _ T R mu }.
 Arguments s_finite {d T R} _.
 
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `isSFinite.Build`")]
-Notation "Measure_isSFinite_subdef.Build" := (@isSFinite.Build _ _ _ _ _) (only parsing).
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `s_finite`")]
-Notation sfinite_measure_subdef := s_finite (only parsing).
-
 Notation "{ 'sfinite_measure' 'set' T '->' '\bar' R }" :=
   (SFiniteMeasure.type T R) : ring_scope.
 
@@ -3393,10 +3368,6 @@ HB.mixin Record isFinite d (T : semiRingOfSetsType d) (R : numDomainType)
 HB.structure Definition FinNumFun d (T : semiRingOfSetsType d)
   (R : numFieldType) := { k of isFinite _ T R k }.
 
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `isFinite.Build`")]
-Notation "'@SigmaFinite_isFinite.Build' d T R k" :=
-  (@isFinite.Build d T R k) (at level 2, d, T, R, k at next level, only parsing).
-
 HB.structure Definition FiniteMeasure d (T : sigmaRingType d) (R : realType) :=
   { k of @SigmaFiniteMeasure _ _ _ k & isFinite _ T R k }.
 Arguments fin_num_measure {d T R} _.
@@ -3548,10 +3519,6 @@ HB.mixin Record isSubProbability d (T : sigmaRingType d) (R : realType)
 HB.structure Definition SubProbability d (T : measurableType d) (R : realType)
   := {mu of @FiniteMeasure d T R mu & isSubProbability d T R mu }.
 
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `isSubProbability.Build`")]
-Notation "'FiniteMeasure_isSubProbability.Build' d T R P" :=
-  (@isSubProbability.Build d T R P) (at level 2, d, T, R, P at next level, only parsing).
-
 HB.factory Record Measure_isSubProbability d (T : measurableType d)
     (R : realType) (P : set T -> \bar R) of isMeasure _ _ _ P :=
   { sprobability_setT : P setT <= 1%E }.
diff --git a/theories/probability.v b/theories/probability.v
index 4ce3d273a4..d7c5b6d228 100644
--- a/theories/probability.v
+++ b/theories/probability.v
@@ -263,7 +263,7 @@ Proof. by rewrite unlock. Qed.
 Lemma expectation_fin_num (X : T -> R) : X \in Lfun P 1 ->
   'E_P[X] \is a fin_num.
 Proof.
-by move=> ?; rewrite unlock integral_fune_fin_num//; exact/Lfun1_integrable.
+by move=> ?; rewrite unlock integrable_fin_num//; exact/Lfun1_integrable.
 Qed.
 
 Lemma expectation_cst r : 'E_P[cst r] = r%:E.
diff --git a/theories/realfun.v b/theories/realfun.v
index 214fa3aadc..9051299acf 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -2016,23 +2016,23 @@ move=> /nonincreasing_funN ndNf abs; have := nondecreasing_variation ndNf abs.
 by rewrite opprK addrC => <-; rewrite variationN.
 Qed.
 
-Lemma variationD a b c f s t : a <= c -> c <= b ->
+Lemma variation_cat a b c f s t : a <= c -> c <= b ->
   itv_partition a c s -> itv_partition c b t ->
-  variation a c f s + variation c b f t = variation a b f (s ++ t).
+  variation a b f (s ++ t) = variation a c f s + variation c b f t.
 Proof.
 rewrite le_eqVlt => /predU1P[<-{c} cb|ac].
   by move=> /itv_partitionxx ->; rewrite variation_nil add0r.
 rewrite le_eqVlt => /predU1P[<-{b}|cb].
   by move=> ? /itv_partitionxx ->; rewrite variation_nil addr0 cats0.
-move=> acs cbt; rewrite /variation /= [in RHS]/index_iota subn0 size_cat.
-rewrite iotaD add0n big_cat/= -[in X in _ = X + _](subn0 (size s)); congr +%R.
+move=> acs cbt; rewrite /variation /= [in LHS]/index_iota subn0 size_cat.
+rewrite iotaD add0n big_cat/= -[in X in X + _ = _](subn0 (size s)); congr +%R.
   rewrite -/(index_iota 0 (size s)) 2!big_nat.
   apply: eq_bigr => k /[!leq0n] /= ks.
   rewrite nth_cat ks -cat_cons nth_cat /= ltnS (ltnW ks).
   by rewrite !(set_nth_default b c)//= ltnS ltnW.
-rewrite -[in RHS](addnK (size s) (size t)).
+rewrite -[in LHS](addnK (size s) (size t)).
 rewrite -/(index_iota (size s) (size t + size s)).
-rewrite -{1}[in RHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr.
+rewrite -{1}[in LHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr.
 move=> k /[!leq0n]/= kt.
 rewrite nth_cat {1}(addnC k) -ltn_subRL subnn ltn0 addnK.
 case: k kt => [t0 /=|k kt].
@@ -2152,9 +2152,9 @@ have waW : w <= a := ltW wa.
 case: ifPn => [|] nXA.
   move/eqP : nXA itvxt itvxb => -> itvat itvt /= ta.
   rewrite -[_ :: t]cat1s -[_ :: s]cat1s.
-  rewrite -?(@variationD _ _ a)//; [|exact: itv_partition1..].
+  rewrite ?(@variation_cat _ _ a)//; [|exact: itv_partition1..].
   by rewrite lerD// IH.
-move=> xts; rewrite -[_ :: s]cat1s -(@variationD _ _ a) => //; last first.
+move=> xts; rewrite -[_ :: s]cat1s (@variation_cat _ _ a) => //; last first.
   exact: itv_partition1.
 have [y [s' s'E]] : exists y s', s = y :: s'.
   by case: {itvas itvws IH} s xts => // y s' ?; exists y, s'.
@@ -2162,10 +2162,12 @@ apply: (@le_trans _ _ (variation w b f s)).
   rewrite IH//.
   case: itvws => /= /andP[_]; rewrite s'E /= => /andP[ay ys' lyb].
   by split => //; rewrite (path_lt_head wa)//= ys' andbT.
-by rewrite variationD //; [exact: le_variation | exact: itv_partition1].
+by rewrite -variation_cat//; [exact: le_variation | exact: itv_partition1].
 Qed.
 
 End variation.
+#[deprecated(since="mathcomp-analysis 1.12.0", note="use `variation_cat` instead")]
+Notation variationD := variation_cat (only parsing).
 
 Section bounded_variation.
 Context {R : realType}.
@@ -2354,7 +2356,7 @@ have H s t : itv_partition a c s -> itv_partition c b t ->
   exists (variation a b f (s ++ t))%:E.
     eexists; last reflexivity.
     by exists (s ++ t) => //; exact: itv_partition_cat acs cbt.
-  by rewrite variationD// ltW.
+  by rewrite -variation_cat// ltW.
 rewrite [leRHS]ereal_sup_EFin//; last first.
   by apply: variations_neq0; rewrite (lt_trans ac).
 have acf : BV a c f := bounded_variationl (ltW ac) (ltW cb) abf.
@@ -2366,7 +2368,7 @@ rewrite -EFinD -sup_sumE; last 2 first.
   by split => //; exact: variations_neq0.
 apply: le_sup.
 - move=> r/= [s [l' acl' <-{s}]] [t [l cbl] <-{t} <-{r}].
-  exists (variation a b f (l' ++ l)); split; last by rewrite variationD// ltW.
+  exists (variation a b f (l' ++ l)); split; last by rewrite -variation_cat// ltW.
   exact/variations_variation/(itv_partition_cat acl' cbl).
 - have [r acfr] := variations_neq0 f ac.
   have [s cbfs] := variations_neq0 f cb.
@@ -2406,7 +2408,7 @@ exists (variation a c f (itv_partitionL l c)).
   by apply: variations_variation; exact: itv_partitionLP pacl.
 exists (variation c b f (itv_partitionR l c)).
   by apply: variations_variation; exact: itv_partitionRP pacl.
-by rewrite variationD// ?ltW//;
+by rewrite -variation_cat// ?ltW//;
   [exact: itv_partitionLP pacl|exact: itv_partitionRP pacl].
 Qed.
 
@@ -2540,7 +2542,7 @@ move: xt; rewrite le_eqVlt => /predU1P[->|xt].
   by rewrite total_variationxx/=.
 have : variation x b f (i :: j) <= variation x t f (t :: nil) +
                                    variation t b f (i :: j).
-  rewrite variationD//; last 2 first.
+  rewrite -variation_cat//; last 2 first.
     exact: itv_partition1.
     by rewrite /itv_partition/= ti ij ijb.
   exact: le_variation.