fixes #1315

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -100,6 +100,9 @@
 - in `normedtype.v`:
   + lemmas `ninfty`, `cvgy_compNP`
 
+- new file `measurable_realfun.v`
+  + with as contents the first half of the file `lebesgue_measure.v`
+
 ### Changed
 
 - in `lebesgue_integral.v`
@@ -126,6 +129,9 @@
 - in `normedtype.v`:
   + lemma `cvgyNP` renamed to `cvgNy_compN` and generalized
 
+- file `lebesgue_measure.v`
+  + first half moved to a new file `measurable_realfun.v`
+
 ### Renamed
 
 - in `measure.v`
@@ -232,6 +238,22 @@
     `__deprecated__dvg_ereal_cvg`, `__deprecated__ereal_cvg_real`
     (were deprecated since 0.6.0)
 
+- in `derive.v`:
+  + notations `le0r_cvg_map`, `ler0_cvg_map`, `ler_cvg_map`
+    (deprecated since 0.6.0)
+  + lemmas `__deprecated__le0r_cvg_map`, `__deprecated__ler0_cvg_map`,
+    `__deprecated__ler_cvg_map`
+    (deprecated since 0.6.0)
+
+- in `normedtype.v`
+  + notations `cvg_distP`, `cvg_distW`, `continuous_cvg_dist`, `cvg_dist2P`,
+    `cvg_gt_ge`, `cvg_lt_le_`, `linear_bounded0`
+    (deprecated since 0.6.0)
+  + lemmas `__deprecated__cvg_distW`, `__deprecated__continuous_cvg_dist`,
+    `__deprecated__cvg_gt_ge`, `__deprecated__cvg_lt_le`,
+    `__deprecated__linear_bounded0 `
+    (deprecated since 0.6.0)
+
 ### Infrastructure
 
 ### Misc

_CoqProject

@@ -77,6 +77,7 @@ theories/sequences.v
 theories/exp.v
 theories/trigo.v
 theories/esum.v
+theories/measurable_realfun.v
 theories/lebesgue_measure.v
 theories/lebesgue_stieltjes_measure.v
 theories/forms.v

theories/Make

@@ -44,6 +44,7 @@ sequences.v
 exp.v
 trigo.v
 esum.v
+measurable_realfun.v
 lebesgue_measure.v
 forms.v
 derive.v

theories/derive.v

@@ -1463,31 +1463,6 @@ by apply: xe_A => //; rewrite eq_sym.
 Qed.
 Arguments cvg_at_leftE {R V} f x.
 
-Lemma __deprecated__le0r_cvg_map (R : realFieldType) (T : topologicalType)
-  (F : set_system T) (FF : ProperFilter F) (f : T -> R) :
-  (\forall x \near F, 0 <= f x) -> cvg (f @ F) -> 0 <= lim (f @ F).
-Proof. by move=> ? ?; rewrite limr_ge. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="generalized by `limr_ge`")]
-Notation le0r_cvg_map := __deprecated__le0r_cvg_map (only parsing).
-
-Lemma __deprecated__ler0_cvg_map (R : realFieldType) (T : topologicalType)
-  (F : set_system T) (FF : ProperFilter F) (f : T -> R) :
-  (\forall x \near F, f x <= 0) -> cvg (f @ F) -> lim (f @ F) <= 0.
-Proof. by move=> ? ?; rewrite limr_le. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="generalized by `limr_le`")]
-Notation ler0_cvg_map := __deprecated__ler0_cvg_map (only parsing).
-
-Lemma __deprecated__ler_cvg_map (R : realFieldType) (T : topologicalType)
-  (F : set_system T) (FF : ProperFilter F) (f g : T -> R) :
-  (\forall x \near F, f x <= g x) -> cvg (f @ F) -> cvg (g @ F) ->
-  lim (f @ F) <= lim (g @ F).
-Proof. by move=> ? ? ?; rewrite ler_lim. Qed.
-#[deprecated(since="mathcomp-analysis 0.6.0",
-  note="subsumed by `ler_lim`")]
-Notation ler_cvg_map := __deprecated__ler_cvg_map (only parsing).
-
 Lemma derive1_at_max (R : realFieldType) (f : R -> R) (a b c : R) :
   a <= b -> (forall t, t \in `]a, b[%R -> derivable f t 1) -> c \in `]a, b[%R ->
   (forall t, t \in `]a, b[%R -> f t <= f c) -> is_derive c 1 f 0.