From 34c7bcf3a17b9640fd4fe4eebba5ff71973bf57c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 5 Jan 2024 13:31:33 +0900 Subject: [PATCH 1/3] fixes #1131 --- CHANGELOG_UNRELEASED.md | 22 ++++++++++++++++++++++ theories/derive.v | 4 ++-- theories/lebesgue_measure.v | 9 +++------ theories/normedtype.v | 13 +++++++------ theories/topology.v | 16 +++++++++------- 5 files changed, 43 insertions(+), 21 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 15dd9a1e6..446d4b491 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -15,6 +15,28 @@ ### Changed + +- in `normedtype.v`: + + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns + duplicate-free lists of indices + +- moved from `lebesgue_integral.v` to `measure.v`: + + definition `ae_eq` + + lemmas + `ae_eq0`, + `ae_eq_comp`, + `ae_eq_funeposneg`, + `ae_eq_refl`, + `ae_eq_trans`, + `ae_eq_sub`, + `ae_eq_mul2r`, + `ae_eq_mul2l`, + `ae_eq_mul1l`, + `ae_eq_abse` + +- in `topology.v`: + + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}` + ### Renamed ### Generalized diff --git a/theories/derive.v b/theories/derive.v index ccce3ec2d..1ee9cf8d5 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -671,7 +671,7 @@ Qed. Lemma linear_lipschitz (V' W' : normedModType R) (f : {linear V' -> W'}) : continuous f -> exists2 k, k > 0 & forall x, `|f x| <= k * `|x|. Proof. -move=> /(_ 0); rewrite linear0 => /(_ _ (nbhsx_ballx 0 1%:pos)). +move=> /(_ 0); rewrite linear0 => /(_ _ (nbhsx_ballx _ _ ltr01)). move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x. have [|xn0] := real_le0P (normr_real x). by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0. @@ -740,7 +740,7 @@ Lemma bilinear_schwarz (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) : continuous (fun p => f p.1 p.2) -> exists2 k, k > 0 & forall u v, `|f u v| <= k * `|u| * `|v|. Proof. -move=> /(_ 0); rewrite linear0r => /(_ _ (nbhsx_ballx 0 1%:pos)). +move=> /(_ 0); rewrite linear0r => /(_ _ (nbhsx_ballx _ _ ltr01)). move=> /nbhs_ballP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v. have [|un0] := real_le0P (normr_real u). by rewrite normr_le0 => /eqP->; rewrite linear0l !normr0 mulr0 mul0r. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index b298482b3..0de7bf9e0 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1950,7 +1950,7 @@ have finDn n : mu (Dn n) \is a fin_num. by rewrite le_measure// ?inE//=; [exact: mDn|exact: subIsetl]. have finD : mu D \is a fin_num by rewrite fin_num_abs gee0_abs. rewrite -[mu D]fineK// => /fine_cvg/(_ (interior (ball (fine (mu D)) eps)))[]. - exact/nbhs_interior/(nbhsx_ballx _ (PosNum epspos)). + exact/nbhs_interior/nbhsx_ballx. move=> n _ /(_ _ (leqnn n))/interior_subset muDN. exists (-n%:R, n%:R)%R; rewrite measureD//=. move: muDN; rewrite /ball/= /ereal_ball/= -fineB//=; last exact: finDn. @@ -2089,9 +2089,7 @@ have mE k n : measurable (E k n). have nEcvg x k : exists n, A x -> (~` (E k n)) x. case : (pselect (A x)); last by move => ?; exists point. move=> Ax; have [] := fptwsg _ Ax (interior (ball (g x) (k.+1%:R^-1))). - apply: open_nbhs_nbhs; split; first exact: open_interior. - have ki0 : ((0:R) < k.+1%:R^-1)%R by rewrite invr_gt0. - rewrite (_ : k.+1%:R^-1 = (PosNum ki0)%:num ) //; exact: nbhsx_ballx. + by apply: open_nbhs_nbhs; split; [exact: open_interior|exact: nbhsx_ballx]. move=> N _ Nk; exists N.+1 => _; rewrite /E setC_bigcup => i /= /ltnW Ni. apply/not_andP; right; apply/negP; rewrite /h -real_ltNge // distrC. by case: (Nk _ Ni) => _/posnumP[?]; apply; exact: ball_norm_center. @@ -2108,8 +2106,7 @@ have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E. - by apply: bigcap_measurable => ?. case/fine_cvg/(_ (interior (ball (0:R) ek))%R). apply: open_nbhs_nbhs; split; first exact: open_interior. - have ekpos : (0 < ek)%R by rewrite divr_gt0 // divr_gt0. - by move: ek ekpos => _/posnumP[ek]; exact: nbhsx_ballx. + by apply: nbhsx_ballx; rewrite !divr_gt0. move=> N _ /(_ N (leqnn _))/interior_subset muEN; exists N; move: muEN. rewrite /ball /= distrC subr0 ger0_norm // -[x in x < _]fineK ?ge0_fin_numE//. by apply:(le_lt_trans _ finA); apply le_measure; rewrite ?inE// => ? [? _ []]. diff --git a/theories/normedtype.v b/theories/normedtype.v index 75a71e00d..9fa6e6434 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1857,7 +1857,7 @@ Lemma dnbhs0_le e : 0 < e -> \forall x \near (0 : V)^', `|x| <= e. Proof. by move=> e_gt0; apply: cvg_within; apply: nbhs0_le. Qed. Lemma nbhs_norm_ball x (eps : {posnum R}) : nbhs_norm x (ball x eps%:num). -Proof. rewrite nbhs_nbhs_norm; by apply: nbhsx_ballx. Qed. +Proof. by rewrite nbhs_nbhs_norm; exact: nbhsx_ballx. Qed. Lemma nbhsDl (P : set V) (x y : V) : (\forall z \near (x + y), P z) <-> (\near x, P (x + y)). @@ -4043,9 +4043,9 @@ have xyab : (edist (x, y) <= edist (x, a) + edist (a, b) + edist (y, b))%E. rewrite (edist_sym y b) -addeA. by rewrite (le_trans (@edist_triangle _ a _))// ?lee_add// ?edist_triangle. have xafin : edist (x, a) \is a fin_num. - by apply/edist_finP; exists 1 =>//; near: a; apply: (nbhsx_ballx _ 1%:pos). + by apply/edist_finP; exists 1 =>//; near: a; exact: nbhsx_ballx. have ybfin : edist (y, b) \is a fin_num. - by apply/edist_finP; exists 1 =>//; near: b; apply: (nbhsx_ballx _ 1%:pos). + by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx. have abfin : edist (a, b) \is a fin_num. by rewrite ge0_fin_numE// (le_lt_trans abxy) ?lte_add_pinfty// -ge0_fin_numE. have xyabfin: (edist (x, y) - edist (a, b))%E \is a fin_num @@ -4053,7 +4053,7 @@ have xyabfin: (edist (x, y) - edist (a, b))%E \is a fin_num rewrite -fineB// -fine_abse// -lee_fin fineK ?abse_fin_num//. rewrite (@le_trans _ _ (edist (x, a) + edist (y, b))%E)//; last first. by rewrite [eps%:num]splitr/= EFinD lee_add//; apply: edist_fin => //=; - [near: a | near: b]; apply: (nbhsx_ballx _ (_ / _)%:pos). + [near: a | near: b]; exact: nbhsx_ballx. have [ab_le_xy|/ltW xy_le_ab] := leP (edist (a, b)) (edist (x, y)). by rewrite gee0_abs ?subre_ge0// lee_subl_addr// addeAC. rewrite lee0_abs ?sube_le0// oppeB ?fin_num_adde_defr//. @@ -4145,7 +4145,7 @@ have fwfin : \forall w \near z, edist_inf w \is a fin_num. rewrite fin_numD fz_fin andbT; apply/edist_finP; exists 1 => //. exact/ball_sym. split => //; apply/cvgrPdist_le => _/posnumP[eps]. -have : nbhs z (ball z eps%:num) by apply: nbhsx_ballx. +have : nbhs z (ball z eps%:num) by exact: nbhsx_ballx. apply: filter_app; near_simpl; move: fwfin; apply: filter_app. near=> t => tfin /= /[dup] ?. have ztfin : edist (z, t) \is a fin_num by apply/edist_finP; exists eps%:num. @@ -5614,7 +5614,8 @@ move=> x clAx; have abx : x \in `[a, b]. by apply: interval_closed; have /closureI [] := clAx. split=> //; have /sabUf [i Di fx] := abx. have /fop := Di; rewrite openE => /(_ _ fx) [_ /posnumP[e] xe_fi]. -have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] := nbhsx_ballx x e. +have /clAx [y [[aby [E sD [sayUf _]]] xe_y]] := + nbhsx_ballx x e%:num ltac:(by []). exists (i |` E)%fset; first by move=> j /fset1UP[->|/sD] //; rewrite inE. split=> [z axz|]; last first. exists i; first by rewrite /= !inE eq_refl. diff --git a/theories/topology.v b/theories/topology.v index 31b5854ff..0e5b4bbc7 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5154,13 +5154,13 @@ Lemma ball_triangle (y x z : M) (e1 e2 : R) : ball x e1 y -> ball y e2 z -> ball x (e1 + e2) z. Proof. exact: PseudoMetric.ball_triangle. Qed. -Lemma nbhsx_ballx (x : M) (eps : {posnum R}) : nbhs x (ball x eps%:num). -Proof. by apply/nbhs_ballP; exists eps%:num => /=. Qed. +Lemma nbhsx_ballx (x : M) (eps : R) : 0 < eps -> nbhs x (ball x eps). +Proof. by move=> e0; apply/nbhs_ballP; exists eps. Qed. Lemma open_nbhs_ball (x : M) (eps : {posnum R}) : open_nbhs x ((ball x eps%:num)^°). Proof. split; first exact: open_interior. -by apply: nbhs_singleton; apply: nbhs_interior; apply:nbhsx_ballx. +by apply: nbhs_singleton; apply: nbhs_interior; exact: nbhsx_ballx. Qed. Lemma le_ball (x : M) (e1 e2 : R) : e1 <= e2 -> ball x e1 `<=` ball x e2. @@ -5175,8 +5175,7 @@ apply: Build_ProperFilter; rewrite -entourage_ballE => A [_/posnumP[e] sbeA]. by exists (point, point); apply: sbeA; apply: ballxx. Qed. -Lemma near_ball (y : M) (eps : {posnum R}) : - \forall y' \near y, ball y eps%:num y'. +Lemma near_ball (y : M) (eps : R) : 0 < eps -> \forall y' \near y, ball y eps y'. Proof. exact: nbhsx_ballx. Qed. Lemma dnbhs_ball (a : M) (e : R) : (0 < e)%R -> a^' (ball a e `\ a). @@ -5234,6 +5233,9 @@ End pseudoMetricType_numDomainType. #[global] Hint Resolve close_refl : core. Arguments close_cvg {T} F1 F2 {FF2} _. +Arguments nbhsx_ballx {R M} x eps. +Arguments near_ball {R M} y eps. + #[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `cvg_ball`")] Notation app_cvg_locally := cvg_ball (only parsing). @@ -6252,8 +6254,8 @@ Lemma Rhausdorff (R : realFieldType) : hausdorff_space R. Proof. move=> x y clxy; apply/eqP; rewrite eq_le. apply/in_segment_addgt0Pr => _ /posnumP[e]. -rewrite in_itv /= -ler_distl; set he := (e%:num / 2)%:pos. -have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x he) (nbhsx_ballx y he). +rewrite in_itv /= -ler_distl; have he : 0 < (e%:num / 2) by []. +have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x _ he) (nbhsx_ballx y _ he). have := ball_triangle yz_he (ball_sym zx_he). by rewrite -mulr2n -mulr_natr divfK // => /ltW. Qed. From a94cd43a6a23c502b7c659e440a04d26d5afe76c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jan 2024 22:21:04 +0900 Subject: [PATCH 2/3] fix changelog --- CHANGELOG_UNRELEASED.md | 19 ------------------- 1 file changed, 19 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 446d4b491..f96118e53 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,25 +14,6 @@ + `sigma_finite_measure` instance on product measure `\x` ### Changed - - -- in `normedtype.v`: - + lemmas `vitali_lemma_finite` and `vitali_lemma_finite_cover` now returns - duplicate-free lists of indices - -- moved from `lebesgue_integral.v` to `measure.v`: - + definition `ae_eq` - + lemmas - `ae_eq0`, - `ae_eq_comp`, - `ae_eq_funeposneg`, - `ae_eq_refl`, - `ae_eq_trans`, - `ae_eq_sub`, - `ae_eq_mul2r`, - `ae_eq_mul2l`, - `ae_eq_mul1l`, - `ae_eq_abse` - in `topology.v`: + lemmas `nbhsx_ballx` and `near_ball` take a parameter of type `R` instead of `{posnum R}` From 52928064c23bb3f48dd1921eddef44f3c7744b6c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jan 2024 23:09:39 +0900 Subject: [PATCH 3/3] fix --- theories/topology.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/topology.v b/theories/topology.v index 0e5b4bbc7..ebfcbd749 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -6257,7 +6257,7 @@ apply/in_segment_addgt0Pr => _ /posnumP[e]. rewrite in_itv /= -ler_distl; have he : 0 < (e%:num / 2) by []. have [z [zx_he yz_he]] := clxy _ _ (nbhsx_ballx x _ he) (nbhsx_ballx y _ he). have := ball_triangle yz_he (ball_sym zx_he). -by rewrite -mulr2n -mulr_natr divfK // => /ltW. +by rewrite -mulr2n -(mulr_natr (_ / _) 2) divfK// => /ltW. Qed. Section RestrictedUniformTopology.