Closed ball0 20250911 (#1717)

* minor generalization

* rename closure_ball

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -31,6 +31,8 @@
   + definition `parse`, `print`
   + number notations in scopes `ereal_dual_scope` and `ereal_scope`
   + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope`
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `le0_ball0`
 
 ### Changed
 
@@ -42,10 +44,19 @@
   + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
   + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
 
+- moved from `vitali_lemma.v` to `pseudometric_normed_Zmodule.v` and renamed:
+  + `closure_ball` -> `closure_ballE`
+
 ### Renamed
 
 ### Generalized
 
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `closed_ball0` (`realFieldType` -> `pseudoMetricNormedZmodType`)
+  + lemmas `closed_ball_closed`, `subset_closed_ball` (`realFieldType` -> `numDomainType`)
+  + lemma `subset_closure_half` (`realFieldType` -> `numFieldType`)
+  + lemma `le_closed_ball` (`pseudoMetricNormedZmodType` -> `pseudoMetricType`)
+
 - in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):
   + lemma `right_continuousW`
   + record `isCumulative`

theories/lebesgue_measure.v

@@ -1350,8 +1350,8 @@ apply: le_trans; apply: lee_nneseries => //; first by move=> *; exact: esum_ge0.
 move=> n _.
 rewrite -(set_mem_set (F n)) -nneseries_esum// -nneseries_esum// -nneseriesZl//.
 apply: lee_nneseries => // m mFn.
-rewrite (ballE (is_ballB m))// closure_ball lebesgue_measure_closed_ball//.
-rewrite scale_ballE// closure_ball lebesgue_measure_closed_ball//.
+rewrite (ballE (is_ballB m))// closure_ballE lebesgue_measure_closed_ball//.
+rewrite scale_ballE// closure_ballE lebesgue_measure_closed_ball//.
 by rewrite -EFinM mulrnAr.
 Qed.
 
@@ -1390,7 +1390,7 @@ Let vitali_cover_mclosure (F : set nat) k :
   vitali_cover A B F -> (R.-ocitv.-measurable).-sigma.-measurable (closure (B k)).
 Proof.
 case => + _ => /(_ k)/ballE ->.
-by rewrite closure_ball; exact: measurable_closed_ball.
+by rewrite closure_ballE; exact: measurable_closed_ball.
 Qed.
 
 Let vitali_cover_measurable (F : set nat) k :
@@ -1452,7 +1452,7 @@ have muGSfin C : C `<=` G -> mu (\bigcup_(k in C) closure (B k)) \is a fin_num.
   apply: lee_nneseries => // n _.
   case: ifPn => [/set_mem nC|]; last by rewrite measure0.
   rewrite (vitali_cover_ballE _ ABF) ifT; last exact/mem_set/CG.
-  by rewrite closure_ball lebesgue_measure_closed_ball// lebesgue_measure_ball.
+  by rewrite closure_ballE lebesgue_measure_closed_ball// lebesgue_measure_ball.
 have muGfin : mu (\bigcup_(k in G) closure (B k)) \is a fin_num.
   by rewrite -(bigB0 G) muGSfin.
 have [c Hc] : exists c : {posnum R},
@@ -1540,8 +1540,8 @@ have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num).
       apply: lee_sum => //= i /G0G'r [iG rBi].
       rewrite -[leRHS]fineK//; last first.
         rewrite (vitali_cover_ballE _ ABF).
-        by rewrite closure_ball lebesgue_measure_closed_ball.
-      rewrite (vitali_cover_ballE _ ABF) closure_ball.
+        by rewrite closure_ballE lebesgue_measure_closed_ball.
+      rewrite (vitali_cover_ballE _ ABF) closure_ballE.
       by rewrite lebesgue_measure_closed_ball// fineK// lee_fin mulr2n ler_wpDl.
     rewrite le_measure? inE//; last exact: bigcup_subset.
     - by apply: bigcup_measurable => k _; exact: vitali_cover_mclosure ABF.
@@ -1557,7 +1557,7 @@ have bigBG_fin (r : {posnum R}) : finite_set (bigB G r%:num).
       move/trivIsetP : tB => /(_ _ _ Gi Gj ij).
       by apply: subsetI_eq0 => //=; exact: subset_closure.
     rewrite /= lee_nneseries// => n _.
-    rewrite (vitali_cover_ballE _ ABF)// closure_ball.
+    rewrite (vitali_cover_ballE _ ABF)// closure_ballE.
     by rewrite lebesgue_measure_closed_ball// lebesgue_measure_ball.
   rewrite le_measure? inE//.
   + by apply: bigcup_measurable => k _; exact: vitali_cover_measurable ABF.

theories/measurable_realfun.v

@@ -334,8 +334,7 @@ Proof. by rewrite ball_itv; exact: measurable_itv. Qed.
 
 Lemma measurable_closed_ball (x : R) r : measurable (closed_ball x r).
 Proof.
-have [r0|r0] := leP r 0; first by rewrite closed_ball0.
-rewrite closed_ball_itv//.
+by have [r0|r0] := leP r 0; [rewrite closed_ball0|rewrite closed_ball_itv].
 Qed.
 
 End salgebra_R_ssets.

theories/normedtype_theory/pseudometric_normed_Zmodule.v

@@ -400,6 +400,18 @@ Arguments cvgr0_norm_le {_ _ _ F FF}.
 #[global] Hint Extern 0 (is_true (`|?x| <= _)) => match goal with
   H : x \is_near _ |- _ => solve[near: x; now apply: cvgr0_norm_le] end : core.
 
+Section pseudoMetricNormedZmod_realDomainType.
+
+Lemma le0_ball0 (R : realDomainType) (V : pseudoMetricNormedZmodType R) (a : V) (r : R) :
+  r <= 0 -> ball a r = set0.
+Proof.
+move=> r0; rewrite -subset0 => y.
+rewrite -ball_normE /ball_/= ltNge => /negP; apply.
+by rewrite (le_trans r0).
+Qed.
+
+End pseudoMetricNormedZmod_realDomainType.
+
 Section pseudoMetricNormedZmod_numFieldType.
 Variables (R : numFieldType) (V : pseudoMetricNormedZmodType R).
 
@@ -420,10 +432,11 @@ Local Hint Extern 0 (hausdorff_space _) => solve[apply: norm_hausdorff] : core.
 (*       i.e. where the generic lemma is applied, *)
 (*            check that norm_hausdorff is not used in a hard way *)
 
-Lemma norm_closeE (x y : V): close x y = (x = y). Proof. exact: closeE. Qed.
+Lemma norm_closeE (x y : V) : close x y = (x = y). Proof. exact: closeE. Qed.
 Lemma norm_close_eq (x y : V) : close x y -> x = y. Proof. exact: close_eq. Qed.
 
-Lemma norm_cvg_unique {F} {FF : ProperFilter F} : is_subset1 [set x : V | F --> x].
+Lemma norm_cvg_unique {F} {FF : ProperFilter F} :
+  is_subset1 [set x : V | F --> x].
 Proof. exact: cvg_unique. Qed.
 
 Lemma norm_cvg_eq (x y : V) : x --> y -> x = y. Proof. exact: (@cvg_eq V). Qed.
@@ -1210,38 +1223,43 @@ Definition closed_ball_ (R : numDomainType) (V : zmodType) (norm : V -> R)
 Definition closed_ball (R : numDomainType) (V : pseudoMetricType R)
   (x : V) (e : R) := closure (ball x e).
 
-Lemma closed_ball0 (R : realFieldType) (a r : R) :
-  r <= 0 -> closed_ball a r = set0.
+Lemma closure_ballE (R : numDomainType) (V : pseudoMetricType R)
+  (c : V) (r : R) : closure (ball c r) = closed_ball c r.
+Proof. by []. Qed.
+
+Lemma closed_ball0 (R : realDomainType) (V : pseudoMetricNormedZmodType R)
+  (v : V) (r : R) : r <= 0 -> closed_ball v r = set0.
 Proof.
-move=> /ball0 r0; apply/seteqP; split => // y.
-by rewrite /closed_ball r0 closure0.
+by move=> r0; rewrite -subset0 => w; rewrite /closed_ball le0_ball0// closure0.
 Qed.
 
 Lemma closed_ballxx (R : numDomainType) (V : pseudoMetricType R) (x : V)
   (e : R) : 0 < e -> closed_ball x e x.
 Proof. by move=> ?; exact/subset_closure/ballxx. Qed.
 
-Lemma closed_ball_closed (R : realFieldType) (V : pseudoMetricType R) (x : V)
+Lemma closed_ball_closed (R : numDomainType) (V : pseudoMetricType R) (x : V)
   (r : R) : closed (closed_ball x r).
 Proof. exact: closed_closure. Qed.
 
-Lemma subset_closed_ball (R : realFieldType) (V : pseudoMetricType R) (x : V)
+Lemma subset_closed_ball (R : numDomainType) (V : pseudoMetricType R) (x : V)
   (r : R) : ball x r `<=` closed_ball x r.
 Proof. exact: subset_closure. Qed.
 
-Lemma subset_closure_half (R : realFieldType) (V : pseudoMetricType R) (x : V)
+Lemma subset_closure_half (R : numFieldType) (V : pseudoMetricType R) (x : V)
   (r : R) : 0 < r -> closed_ball x (r / 2) `<=` ball x r.
 Proof.
 move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) [].
   exact: nbhsx_ballx.
 by move=> y [+/ball_sym]; rewrite [t in ball x t z]splitr; apply: ball_triangle.
 Qed.
 
-Lemma le_closed_ball (R : numFieldType) (M : pseudoMetricNormedZmodType R)
+Lemma le_closed_ball (R : numFieldType) (M : pseudoMetricType R)
   (x : M) (e1 e2 : R) : (e1 <= e2)%O -> closed_ball x e1 `<=` closed_ball x e2.
 Proof. by rewrite /closed_ball => le; apply/closure_subset/le_ball. Qed.
 
 End Closed_Ball.
+#[deprecated(since="mathcomp-analysis 1.14.0", note="renamed to `closure_ballE`")]
+Notation closure_ball := closure_ballE (only parsing).
 
 Section limit_composition_pseudometric.
 Context {K : numFieldType} {V : pseudoMetricNormedZmodType K} {T : Type}.

theories/normedtype_theory/vitali_lemma.v

@@ -202,13 +202,6 @@ Lemma is_ball_closure (A : set R) : is_ball A ->
   closure A = closed_ball (cpoint A) (radius A)%:num.
 Proof. by move=> ballA; rewrite /closed_ball -ballE. Qed.
 
-Lemma closure_ball (c r : R) : closure (ball c r) = closed_ball c r.
-Proof.
-have [r0|r0] := leP r 0.
-  by rewrite closed_ball0// ((ball0 _ _).2 r0) closure0.
-by rewrite (is_ball_closure (is_ball_ball _ _)) cpoint_ball// radius_ball ?ltW.
-Qed.
-
 Lemma scale_ballE k x r : 0 <= k -> k *` ball x r = ball x (k * r).
 Proof.
 move=> k0; have [r0|r0] := ltP 0 r.