Fixes 20231108 (#1081)

* fixes #1054

* fixes #1063

* fixes #1055

* fixes #1066

* fixes #1082

CHANGELOG_UNRELEASED.md

@@ -81,6 +81,15 @@
 - in `lebesgue_integral.v`:
   + order of arguments in the lemma `le_abse_integral`
 
+- in `lebesgue_measure.v`:
+  + remove one argument of `lebesgue_regularity_inner_sup`
+
+- in `normedtype.v`:
+  + order of arguments of `squeeze_cvgr`
+
+- moved from `derive.v` to `normedtype.v`:
+  + lemmas `cvg_at_rightE`, `cvg_at_leftE`
+
 ### Renamed
 
 - in `charge.v`

coq-mathcomp-analysis.opam

@@ -29,6 +29,11 @@ tags: [
   "keyword:analysis"
   "keyword:topology"
   "keyword:real numbers"
+  "keyword:differentiation"
+  "keyword:derivative"
+  "keyword:measure theory"
+  "keyword:integration"
+  "keyword:Lebesgue"
   "logpath:mathcomp.analysis"
 ]
 authors: [

coq-mathcomp-classical.opam

@@ -31,6 +31,9 @@ tags: [
   "keyword:classical"
   "keyword:logic"
   "keyword:sets"
+  "keyword:set theory"
+  "keyword:functions"
+  "keyword:cardinal"
   "logpath:mathcomp.classical"
 ]
 authors: [

theories/derive.v

@@ -1351,25 +1351,6 @@ have /(EVT_max leab) [c clr fcmax] : {within `[a, b], continuous (- f)}.
 by exists c => // ? /fcmax; rewrite ler_opp2.
 Qed.
 
-Lemma cvg_at_rightE (R : numFieldType) (V : normedModType R) (f : R -> V) x :
-  cvg (f @ x^') -> lim (f @ x^') = lim (f @ at_right x).
-Proof.
-move=> cvfx; apply/Logic.eq_sym.
-apply: (@cvg_lim _ _ _ (at_right _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
-by exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
-Qed.
-Arguments cvg_at_rightE {R V} f x.
-
-Lemma cvg_at_leftE (R : numFieldType) (V : normedModType R) (f : R -> V) x :
-  cvg (f @ x^') -> lim (f @ x^') = lim (f @ at_left x).
-Proof.
-move=> cvfx; apply/Logic.eq_sym.
-apply: (@cvg_lim _ _ _ (at_left _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
-exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _].
-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 (set T))
   (FF : ProperFilter F) (f : T -> R) :
   (\forall x \near F, 0 <= f x) -> cvg (f @ F) -> 0 <= lim (f @ F).

theories/lebesgue_measure.v

@@ -1819,7 +1819,7 @@ Notation emeasurable_fun_funeneg := measurable_funeneg (only parsing).
 Notation measurable_fun_lim_esup := measurable_fun_limn_esup (only parsing).
 
 Section lebesgue_regularity.
-Context {d : measure_display} {R : realType}.
+Context {R : realType}.
 Let mu := [the measure _ _ of @lebesgue_measure R].
 
 Local Open Scope ereal_scope.
@@ -1977,7 +1977,7 @@ rewrite -{1}(setDKU BA) (@le_trans _ _ (mu B + mu (A `\` B)))//.
 by rewrite lee_add//; [apply: ereal_sup_ub => /=; exists B|exact/ltW].
 Qed.
 
-Lemma lebesgue_regularity_inner_sup (D : set R) (eps : R) : measurable D ->
+Lemma lebesgue_regularity_inner_sup (D : set R) : measurable D ->
   mu D = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` D]].
 Proof.
 move=> mD; have [?|] := ltP (mu D) +oo.

theories/normedtype.v

@@ -2719,6 +2719,25 @@ Module Export NbhsNorm.
 Definition nbhs_simpl := (nbhs_simpl,@nbhs_nbhs_norm,@filter_from_norm_nbhs).
 End NbhsNorm.
 
+Lemma cvg_at_rightE (R : numFieldType) (V : normedModType R) (f : R -> V) x :
+  cvg (f @ x^') -> lim (f @ x^') = lim (f @ x^'+).
+Proof.
+move=> cvfx; apply/Logic.eq_sym.
+apply: (@cvg_lim _ _ _ (at_right _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
+by exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
+Qed.
+Arguments cvg_at_rightE {R V} f x.
+
+Lemma cvg_at_leftE (R : numFieldType) (V : normedModType R) (f : R -> V) x :
+  cvg (f @ x^') -> lim (f @ x^') = lim (f @ x^'-).
+Proof.
+move=> cvfx; apply/Logic.eq_sym.
+apply: (@cvg_lim _ _ _ (at_left _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
+exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _].
+by apply: xe_A => //; rewrite eq_sym.
+Qed.
+Arguments cvg_at_leftE {R V} f x.
+
 (* TODO: generalize to R : numFieldType *)
 Section hausdorff.
 
@@ -5007,7 +5026,7 @@ Section FilterRealType.
 Context {T : Type} {a : set (set T)} {Fa : Filter a} {R : realFieldType}.
 Implicit Types f g h : T -> R.
 
-Lemma squeeze_cvgr f g h : (\near a, f a <= g a <= h a) ->
+Lemma squeeze_cvgr f h g : (\near a, f a <= g a <= h a) ->
   forall (l : R), f @ a --> l -> h @ a --> l -> g @ a --> l.
 Proof.
 move=> fgh l lfa lga; apply/cvgrPdist_lt => e e_gt0.

theories/sequences.v

@@ -979,7 +979,7 @@ Lemma cvg_expr (R : archiFieldType) (z : R) :
   `|z| < 1 -> (GRing.exp z : R ^nat) --> (0 : R).
 Proof.
 move=> Nz_lt1; apply/norm_cvg0P; pose t := (1 - `|z|).
-apply: (@squeeze_cvgr _ _ _ _ (cst 0) _ (t^-1 *: @harmonic R)); last 2 first.
+apply: (@squeeze_cvgr _ _ _ _ (cst 0) (t^-1 *: @harmonic R)); last 2 first.
 - exact: cvg_cst.
 - by rewrite -(scaler0 _ t^-1); exact: (cvgZr cvg_harmonic).
 near=> n; rewrite normr_ge0 normrX/= ler_pdivl_mull ?subr_gt0//.