From 3fc4d47cf94e6b77a35df79af3ac35302ed7b79d Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 11 Sep 2025 12:07:10 +0900 Subject: [PATCH 1/2] minor generalization --- CHANGELOG_UNRELEASED.md | 8 +++++ theories/measurable_realfun.v | 3 +- .../pseudometric_normed_Zmodule.v | 32 +++++++++++++------ theories/normedtype_theory/vitali_lemma.v | 3 +- 4 files changed, 32 insertions(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a5849a8539..2c6ab68c4c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 @@ -46,6 +48,12 @@ ### 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` diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index f820cedcf9..8981243a61 100644 --- a/theories/measurable_realfun.v +++ b/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. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 30e6d7511c..9a8ba0429e 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/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,26 +1223,25 @@ 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 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)) []. @@ -1237,7 +1249,7 @@ move:r => _/posnumP[r] z /(_ (ball z ((r%:num/2)%:pos)%:num)) []. 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. diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index fa5daf1df1..276cd6163a 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -204,8 +204,7 @@ 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. +have [r0|r0] := leP r 0; first by rewrite closed_ball0// le0_ball0// closure0. by rewrite (is_ball_closure (is_ball_ball _ _)) cpoint_ball// radius_ball ?ltW. Qed. From 0c05131167ebf1f8d7bbca84910ed8a17eb44efd Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 11 Sep 2025 12:23:45 +0900 Subject: [PATCH 2/2] rename closure_ball --- CHANGELOG_UNRELEASED.md | 3 +++ theories/lebesgue_measure.v | 14 +++++++------- .../pseudometric_normed_Zmodule.v | 6 ++++++ theories/normedtype_theory/vitali_lemma.v | 6 ------ 4 files changed, 16 insertions(+), 13 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 2c6ab68c4c..cb9c201927 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -44,6 +44,9 @@ + 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 diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index a6d9a7356d..00719b349a 100644 --- a/theories/lebesgue_measure.v +++ b/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. diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 9a8ba0429e..07329928f1 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1223,6 +1223,10 @@ 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 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. @@ -1254,6 +1258,8 @@ Lemma le_closed_ball (R : numFieldType) (M : pseudoMetricType R) 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}. diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index 276cd6163a..714e1f6526 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -202,12 +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; first by rewrite closed_ball0// le0_ball0// 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.