Fixes 1992

CHANGELOG_UNRELEASED.md

@@ -264,6 +264,9 @@
 - in `measure_function.v`:
   + `isFinite` -> `isFinNumFun`
 
+- in `topology_structure.v`:
+  + `closure_setC` -> `closureC`
+
 ### Generalized
 
 - in `measurable_structure.v`:
@@ -307,6 +310,26 @@
   + notations `preimage_class`, `image_class`, `sigma_algebra_preimage_class`,
     `sigma_algebra_image_class`, `sigma_algebra_preimage_classE` (deprecated since 1.9.0)
 
+- in `ftc.v`:
+  + lemma `integrable_locally`
+
+- in `lebesgue_Rintegral.v`:
+  + notation `Rintegral_setU_EFin` (deprecated since 1.9.0)
+
+- in `topology_structure.v`:
+  + lemma `closureC_deprecated` (deprecated since 1.7.0)
+
+- in `num_normedtype.v`:
+  + notation `near_in_itv` (deprecated since 1.7.0)
+
+- in `measurable_fun_approximation.v`:
+  + lemma `approximation` (deprecated since 1.8.0)
+  + notations `emeasurable_fun_sum`, `emeasurable_fun_fsum`,
+    `ge0_emeasurable_fun_sum` (deprecated since 1.8.0)
+
+- in `random_variable.v`:
+  + notation `expectationM` (deprecated since 1.8.0)
+
 ### Infrastructure
 
 ### Misc

theories/ftc.v

@@ -68,24 +68,6 @@ Notation mu := (@lebesgue_measure R).
 Local Open Scope ereal_scope.
 Implicit Types (f : R -> R) (a : itv_bound R).
 
-Lemma integrable_locally f (A : set R) : measurable A ->
-  mu.-integrable A (EFin \o f) -> locally_integrable [set: R] (f \_ A).
-Proof.
-move=> mA intf; split.
-- move/integrableP : intf => [mf _].
-  by apply/(measurable_restrictT _ _).1 => //; exact/measurable_EFinP.
-- exact: openT.
-- move=> K _ cK.
-  move/integrableP : intf => [mf].
-  rewrite integral_mkcond/=.
-  under eq_integral do rewrite restrict_EFin restrict_normr.
-  apply: le_lt_trans.
-  apply: ge0_subset_integral => //=; first exact: compact_measurable.
-  apply/measurable_EFinP/measurableT_comp/measurable_EFinP => //=.
-  move/(measurable_restrictT _ _).1 : mf => /=.
-  by rewrite restrict_EFin; exact.
-Qed.
-
 Let FTC0 f a : mu.-integrable setT (EFin \o f) ->
   let F x := (\int[mu]_(t in [set` Interval a (BRight x)]) f t)%R in
   forall x, a < BRight x -> lebesgue_pt f x ->
@@ -345,6 +327,9 @@ Proof. by move=> xu locf F ax fx; exact: (@continuous_FTC1 _ _ _ u). Qed.
 
 End FTC.
 
+#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `integrable_locally_restrict`")]
+Notation integrable_locally := integrable_locally_restrict (only parsing).
+
 Definition parameterized_integral {R : realType}
     (mu : {measure set (measurableTypeR R) -> \bar R})
     a x (f : R -> R) : R :=

theories/lebesgue_integral_theory/lebesgue_Rintegral.v

@@ -189,8 +189,6 @@ by rewrite /Rintegral integralB_EFin// fineB//; exact: integrable_fin_num.
 Qed.
 
 End Rintegral.
-#[deprecated(since="mathcomp-analysis 1.9.0", note="renamed to `Rintegral_setU`")]
-Notation Rintegral_setU_EFin := Rintegral_setU (only parsing).
 #[deprecated(since="mathcomp-analysis 1.10.0", note="renamed to `le_normr_Rintegral`")]
 Notation le_normr_integral := le_normr_Rintegral (only parsing).
 

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.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.
 From mathcomp Require Import interval_inference archimedean finmap.

theories/lebesgue_integral_theory/measurable_fun_approximation.v

@@ -373,15 +373,6 @@ move=> m n mn; rewrite (nnsfun_approxE n) (nnsfun_approxE m).
 exact: nd_approx.
 Qed.
 
-#[deprecated(since="mathcomp-analysis 1.8.0", note="use `nnsfun_approx`, `cvg_nnsfun_approx`, and `nd_nnsfun_approx` instead")]
-Lemma approximation : (forall t, D t -> (0 <= f t)%E) ->
-  exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\
-                        (forall x, D x -> EFin \o g^~ x @ \oo --> f x).
-Proof.
-exists nnsfun_approx; split; [exact: nd_nnsfun_approx|].
-by move=> x Dx; exact: cvg_nnsfun_approx.
-Qed.
-
 End approximation.
 
 Section approximation_sfun.
@@ -565,12 +556,6 @@ Lemma measurable_funeM D (f : T -> \bar R) (k : \bar R) :
 Proof. by move=> mf; exact/(emeasurable_funM _ mf). Qed.
 
 End emeasurable_fun_arith.
-#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `emeasurable_sum`")]
-Notation emeasurable_fun_sum := emeasurable_sum (only parsing).
-#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `emeasurable_fsum`")]
-Notation emeasurable_fun_fsum := emeasurable_fsum (only parsing).
-#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `ge0_emeasurable_sum`")]
-Notation ge0_emeasurable_fun_sum := ge0_emeasurable_sum (only parsing).
 
 Section measurable_sum.
 Context d (T : measurableType d) (R : realType).

theories/measure_theory/measure_function.v

@@ -1407,7 +1407,7 @@ HB.mixin Record isFinNumFun d (T : semiRingOfSetsType d) (R : numDomainType)
 Notation isFinite x1 x2 x3 x4 := (isFinNumFun x1 x2 x3 x4).
 
 Module isFinite.
-#[deprecated(since="mathcomp-analysis 1.117.0", use=isFinNumFun)]
+#[deprecated(since="mathcomp-analysis 1.17.0", use=isFinNumFun)]
 Notation Build x1 x2 x3 x4 := (isFinNumFun.Build x1 x2 x3 x4) (only parsing).
 End isFinite.
 

theories/normedtype_theory/num_normedtype.v

@@ -707,9 +707,6 @@ Lemma near_in_itvNyo :
 Proof. exact: interval_open. Qed.
 
 End near_in_itv.
-#[deprecated(since="mathcomp-analysis 1.7.0",
-  note="use `near_in_itvoo` instead")]
-Notation near_in_itv := near_in_itvoo (only parsing).
 
 Lemma nbhs_infty_gtr {R : archiRealFieldType} (r : R) :
   \forall n \near \oo, r < n%:R.

theories/probability_theory/random_variable.v

@@ -559,8 +559,6 @@ by rewrite IHX//= => Xi XiX; rewrite intX// inE XiX orbT.
 Qed.
 
 End expectation_lemmas.
-#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to `expectationZl`")]
-Notation expectationM := expectationZl (only parsing).
 
 Section tail_expectation_formula.
 Local Open Scope ereal_scope.

theories/topology_theory/topology_structure.v

@@ -894,8 +894,7 @@ exists U => //; apply/(subset_trans UX)/disjoints_subset; rewrite setIC.
 exact/eqP/negbNE/negP/set0P.
 Qed.
 
-(* TODO: rename to closureC after removing the deprecated one *)
-Lemma closure_setC A : closure (~` A) = ~` A°.
+Lemma closureC A : closure (~` A) = ~` A°.
 Proof. by apply: setC_inj; rewrite -interiorC !setCK. Qed.
 
 Lemma interiorS A B : A `<=` B -> A° `<=` B°.
@@ -926,18 +925,15 @@ Lemma closureU A B : closure (A `|` B) = closure A `|` closure B.
 Proof. by apply: setC_inj; rewrite setCU -!interiorC -interiorI setCU. Qed.
 
 Lemma interiorU A B : A° `|` B° `<=` (A `|` B)°.
-Proof.
-by apply: subsetC2; rewrite setCU -!closure_setC setCU; exact: closureI.
-Qed.
+Proof. by apply: subsetC2; rewrite setCU -!closureC setCU; exact: closureI. Qed.
 
 Lemma closureEbigcap A :
   closure A = \bigcap_(x in [set C | closed C /\ A `<=` C]) x.
 Proof. exact: closureE. Qed.
 
-Lemma interiorEbigcup A :
-  A° = \bigcup_(x in [set U | open U /\ U `<=` A]) x.
+Lemma interiorEbigcup A : A° = \bigcup_(x in [set U | open U /\ U `<=` A]) x.
 Proof.
-apply: setC_inj; rewrite -closure_setC closureEbigcap setC_bigcup.
+apply: setC_inj; rewrite -closureC closureEbigcap setC_bigcup.
 rewrite -[RHS](bigcap_image _ setC idfun) /=.
 apply: eq_bigcapl; split => X /=.
   by rewrite -openC -setCS setCK; exists (~` X)=> //; rewrite setCK.
@@ -961,8 +957,7 @@ Qed.
 Lemma closure_open_regclosed A : open A -> regclosed (closure A).
 Proof.
 rewrite /regclosed -(setCK A) openC => cCA.
-rewrite closure_setC -[in RHS]interior_closed_regopen//.
-by rewrite !(closure_setC, interiorC).
+by rewrite closureC -[in RHS]interior_closed_regopen// !(closureC, interiorC).
 Qed.
 
 Lemma interior_closure_idem : @idempotent_fun (set T) (interior \o closure).
@@ -972,12 +967,8 @@ Lemma closure_interior_idem : @idempotent_fun (set T) (closure \o interior).
 Proof. move=> ?; exact/closure_open_regclosed/open_interior. Qed.
 
 End closure_interior_lemmas.
-
-Lemma closureC_deprecated (T : topologicalType) (E : set T) :
-  ~` closure E = \bigcup_(x in [set U | open U /\ U `<=` ~` E]) x.
-Proof. by rewrite -interiorC interiorEbigcup. Qed.
-#[deprecated(since="mathcomp-analysis 1.7.0", note="use `interiorC` and `interiorEbigcup` instead")]
-Notation closureC := closureC_deprecated (only parsing).
+#[deprecated(since="mathcomp-analysis 1.17.0", note="renamed to `closureC`")]
+Notation closure_setC := closureC (only parsing).
 
 Definition dense (T : topologicalType) (S : set T) :=
   forall (O : set T), O !=set0 -> open O -> O `&` S !=set0.