easy gen, rm deprecated (#1773)

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -17,15 +17,51 @@
 
 ### Renamed
 
+- in `probability.v`:
+  + `derivable_oo_continuous_bnd_onemXnMr` -> `derivable_oo_LRcontinuous_onemXnMr`
+
 ### Generalized
 
 - in `lebesgue_integral_under.v`:
   + weaken an hypothesis of lemma `continuity_under_integral`
 
+- in `lebesgue_integrable.v`:
+  + weaken an hypothesis of lemma `finite_measure_integrable_cst`
+
 ### Deprecated
 
 ### Removed
 
+- in `lebesgue_stieltjes_measure.v`:
+  + notation `wlength_sigma_sub_additive` (deprecated since 1.1.0)
+
+- in `constructive_ereal.v`:
+  + notations `gee_pmull`, `gee_addl`, `gee_addr`, `gte_addr`, `gte_addl`,
+    `lte_subl_addr`, `lte_subl_addl`, `lte_subr_addr`, `lte_subr_addl`,
+    `lee_subl_addr`, `lee_subl_addl`, `lee_subr_addr`, `lee_subr_addl`
+    (deprecated since 1.2.0)
+
+- in `signed.v`:
+  + notations `num_le_maxr`, `num_le_maxl`, `num_le_minr`, `num_le_minl`,
+    `num_lt_maxr`, `num_lt_maxl`, `num_lt_minr`, `num_lt_minl`
+    (deprecated since 1.2.0)
+
+- in `measure_function.v`:
+  + notations `g_salgebra_measure_unique_trace`,
+    `g_salgebra_measure_unique_cover`, `g_salgebra_measure_unique`
+    (deprecated since 1.2.0)
+
+- in `measurable_structure.v`:
+  + notations `monotone_class`, `monotone_class_g_salgebra`,
+    `smallest_monotone_classE`, `monotone_class_subset`,
+    `setI_closed_gdynkin_salgebra`, `dynkin_g_dynkin`, `dynkin_monotone`,
+    `salgebraType`
+    (deprecated since 1.2.0)
+
+- in `sequences.v`:
+  + notation `eq_bigsetU_seqD`
+    (deprecated since 1.2.0)
+
 ### Infrastructure
 
 ### Misc

reals/constructive_ereal.v

@@ -2957,32 +2957,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.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.")]
-Notation gee_addl := geeDl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use geeDr instead.")]
-Notation gee_addr := geeDr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use gteDr instead.")]
-Notation gte_addr := gteDr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use gteDl instead.")]
-Notation gte_addl := gteDl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBlDr instead.")]
-Notation lte_subl_addr := lteBlDr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBlDl instead.")]
-Notation lte_subl_addl := lteBlDl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBrDr instead.")]
-Notation lte_subr_addr := lteBrDr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBrDl instead.")]
-Notation lte_subr_addl := lteBrDl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBlDr instead.")]
-Notation lee_subl_addr := leeBlDr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBlDl instead.")]
-Notation lee_subl_addl := leeBlDl (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBrDr instead.")]
-Notation lee_subr_addr := leeBrDr (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBrDl instead.")]
-Notation lee_subr_addl := leeBrDl (only parsing).
 #[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leD` instead.")]
 Notation lte_le_add := lte_leD (only parsing).
 #[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lee_ltD` instead.")]

reals/signed.v

@@ -1130,22 +1130,6 @@ Lemma num_gt_min a x y :
 Proof. by rewrite -comparable_gt_min// real_comparable. Qed.
 
 End MorphReal.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_le_max`")]
-Notation num_le_maxr := num_le_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_ge_max`")]
-Notation num_le_maxl := num_ge_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_le_min`")]
-Notation num_le_minr := num_le_min (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_ge_min`")]
-Notation num_le_minl := num_ge_min (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lt_max`")]
-Notation num_lt_maxr := num_lt_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gt_max`")]
-Notation num_lt_maxl := num_gt_max (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lt_min`")]
-Notation num_lt_minr := num_lt_min (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gt_min`")]
-Notation num_lt_minl := num_gt_min (only parsing).
 
 Section MorphGe0.
 Context {R : numDomainType} {nz : nullity}.

theories/hoelder.v

@@ -1183,11 +1183,11 @@ Variable mu : {finite_measure set T -> \bar R}.
 
 Lemma Lfun_cst c r : cst c \in Lfun mu r%:E.
 Proof.
-rewrite inE; apply/andP; split; rewrite inE//= /finite_norm unlock/Lnorm poweR_lty//.
+rewrite inE/=; apply/andP; split; rewrite inE//=.
+rewrite /finite_norm unlock poweR_lty//.
 under eq_integral => x _/= do rewrite (_ : `|c| `^ r = cst (`|c| `^ r) x)//.
-have /integrableP[_/=] := finite_measure_integrable_cst mu (`|c| `^ r).
-under eq_integral => x _ do rewrite ger0_norm ?powR_ge0//.
-by [].
+apply/integrable_lty => //.
+exact: finite_measure_integrable_cst.
 Qed.
 
 End Lspace_finite_measure.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -391,18 +391,18 @@ rewrite (@le_lt_trans _ _ (mu setT)) ?le_measure ?inE//.
 by rewrite ?ltry ?fin_num_fun_lty//; exact: fin_num_measure.
 Qed.
 
-Lemma finite_measure_integrable_cst k : mu.-integrable [set: T] (EFin \o cst k).
+Lemma finite_measure_integrable_cst A k :
+  measurable A -> mu.-integrable A (EFin \o cst k).
 Proof.
-apply/integrableP; split; first exact/measurable_EFinP.
+move=> mA; apply/integrableP; split; first exact/measurable_EFinP.
 have [k0|k0] := leP 0%R k.
 - under eq_integral do rewrite /= ger0_norm//.
   rewrite lebesgue_integral_nonneg.integral_cstr//= lte_mul_pinfty//.
-  rewrite fin_num_fun_lty//.
-  exact: fin_num_measure.
+  by rewrite -ge0_fin_numE// fin_num_measure.
 - under eq_integral do rewrite /= ltr0_norm//.
   rewrite lebesgue_integral_nonneg.integral_cstr//= lte_mul_pinfty//.
     by rewrite lee_fin lerNr oppr0 ltW.
-  by rewrite fin_num_fun_lty//; exact: fin_num_measure.
+  by rewrite -ge0_fin_numE// fin_num_measure.
 Qed.
 
 End integrable_finite_measure.

theories/lebesgue_stieltjes_measure.v

@@ -506,9 +506,6 @@ HB.instance Definition _ (f : cumulative R R) :=
 End wlength_extension.
 Arguments lebesgue_stieltjes_measure {R}.
 
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `wlength_sigma_subadditive`")]
-Notation wlength_sigma_sub_additive := wlength_sigma_subadditive (only parsing).
-
 Definition measurableTypeR (R : realType) :=
   g_sigma_algebraType R.-ocitv.-measurable.
 

theories/measure_theory/measurable_structure.v

@@ -221,8 +221,6 @@ Definition lambda_system :=
 Definition monotone := ndseq_closed /\ niseq_closed.
 
 End set_systems.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `lambda_system`")]
-Notation monotone_class := lambda_system (only parsing).
 (*#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `setSD_closed`")]
 Notation setD_closed := setSD_closed (only parsing).*)
 #[deprecated(since="mathcomp-analysis 1.9.0", note="renamed `setD_closed`")]
@@ -430,8 +428,6 @@ Proof.
 move=> sDGD; have := smallest_sigma_algebra D G.
 by move=> /(sigma_algebraP sDGD) [sT sD snd sI]; split.
 Qed.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_lambda_system`")]
-Notation monotone_class_g_salgebra := g_sigma_algebra_lambda_system (only parsing).
 
 Lemma smallest_sigma_ring T (G : set (set T)) : sigma_ring <<sr G >>.
 Proof.
@@ -594,8 +590,6 @@ by move=> *; apply HHH_.
 Qed.
 
 End smallest_lambda_system.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `smallest_lambda_system`")]
-Notation smallest_monotone_classE := smallest_lambda_system (only parsing).
 
 Section lambda_system_subset.
 Variables (T : Type) (G : set (set T)) (setIG : setI_closed G) (D : set T).
@@ -613,8 +607,6 @@ rewrite -(@smallest_lambda_system _ _ setIG D) //.
 Qed.
 
 End lambda_system_subset.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `lambda_system_subset`")]
-Notation monotone_class_subset := lambda_system_subset (only parsing).
 
 Section dynkin.
 Variable T : Type.
@@ -740,12 +732,6 @@ exact: g_dynkin_dynkin.
 Qed.
 
 End dynkin_lemmas.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `setI_closed_g_dynkin_g_sigma_algebra`")]
-Notation setI_closed_gdynkin_salgebra := setI_closed_g_dynkin_g_sigma_algebra (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `g_dynkin_dynkin`")]
-Notation dynkin_g_dynkin := g_dynkin_dynkin (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `dynkin_lambda_system`")]
-Notation dynkin_monotone := dynkin_lambda_system (only parsing).
 
 Section trace.
 Variable (T : Type).
@@ -1270,8 +1256,6 @@ Definition sigma_display {T} : set (set T) -> measure_display.
 Proof. exact. Qed.
 
 Definition g_sigma_algebraType {T} (G : set (set T)) := T.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed into `g_sigma_algebraType`")]
-Notation salgebraType := g_sigma_algebraType (only parsing).
 
 Section g_salgebra_instance.
 Variables (T : pointedType) (G : set (set T)).

theories/measure_theory/measure_function.v

@@ -1747,8 +1747,6 @@ Qed.
 
 End g_sigma_algebra_measure_unique_trace.
 Arguments g_sigma_algebra_measure_unique_trace {d R T} G D.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_measure_unique_trace`")]
-Notation g_salgebra_measure_unique_trace := g_sigma_algebra_measure_unique_trace (only parsing).
 
 Definition lim_sup_set T (F : (set T)^nat) := \bigcap_n \bigcup_(j >= n) F j.
 
@@ -1932,10 +1930,6 @@ Qed.
 
 End g_sigma_algebra_measure_unique.
 Arguments g_sigma_algebra_measure_unique {d R T} G.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_measure_unique_cover`")]
-Notation g_salgebra_measure_unique_cover := g_sigma_algebra_measure_unique_cover (only parsing).
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `g_sigma_algebra_measure_unique`")]
-Notation g_salgebra_measure_unique := g_sigma_algebra_measure_unique (only parsing).
 
 Section measure_unique.
 Context d (R : realType) (T : measurableType d).

theories/probability.v

@@ -2191,19 +2191,19 @@ have := @derivableX _ _ (@onem R) n x 1.
 by rewrite fctE; apply; exact: derivableB.
 Qed.
 
-Lemma derivable_oo_continuous_bnd_onemXnMr n x :
-  derivable_oo_continuous_bnd (fun y => `1-y ^+ n * x) 0 1.
+Lemma derivable_oo_LRcontinuous_onemXnMr n x :
+  derivable_oo_LRcontinuous (fun y => `1-y ^+ n * x) 0 1.
 Proof.
 split.
 - by move=> y y01; apply: derivableM => //=; exact: onemXn_derivable.
 - apply: cvgM; last exact: cvg_cst.
   apply: cvg_at_right_filter.
-  apply: (@cvg_comp _ _ _ (fun x => `1-x) (fun x => x ^+ n)).
+  apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).
     by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
   exact: exprn_continuous.
 - apply: cvg_at_left_filter.
   apply: cvgM; last exact: cvg_cst.
-  apply: (@cvg_comp _ _ _ (fun x => `1-x) (fun x => x ^+ n)).
+  apply: (@cvg_comp _ _ _ onem (fun x => x ^+ n)).
     by apply: cvgB; [exact: cvg_cst|exact: cvg_id].
   exact: exprn_continuous.
 Qed.
@@ -2225,12 +2225,14 @@ rewrite (@continuous_FTC2 _ _ (fun x => `1-x ^+ n.+1 / - n.+1%:R))//=.
 - rewrite onem1 expr0n/= mul0r onem0 expr1n mul1r sub0r.
   by rewrite -invrN -2!mulNrn opprK.
 - by apply: continuous_in_subspaceT => x x01; exact: continuous_onemXn.
-- exact: derivable_oo_continuous_bnd_onemXnMr.
+- exact: derivable_oo_LRcontinuous_onemXnMr.
 - move=> x x01; rewrite derive1Mr//; last exact: onemXn_derivable.
   by rewrite derive_onemXn mulrAC divff// mul1r.
 Qed.
 
 End about_onemXn.
+#[deprecated(since="mathcomp-analysis 1.15.0", note="renamed to `derivable_oo_LRcontinuous_onemXnMr`")]
+Notation derivable_oo_continuous_bnd_onemXnMr := derivable_oo_LRcontinuous_onemXnMr (only parsing).
 
 (**md about the function $x \mapsto x^a  (1 - x)^b$ *)
 Section XMonemX.

theories/sequences.v

@@ -364,8 +364,6 @@ by exists i => //; rewrite big_ord_recr/=; right.
 Qed.
 
 End seqD.
-#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed to `nondecreasing_bigsetU_seqD`")]
-Notation eq_bigsetU_seqD := nondecreasing_bigsetU_seqD (only parsing).
 
 Lemma seqDUE {R : realDomainType} n (r : R) :
   (seqDU (fun n => `]r, r + n%:R]) n = `]r + n.-1%:R, r + n%:R])%classic.