From 592f514929f9d41813155b29285556f5c71577dc Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 18 Jan 2024 10:20:04 +0900 Subject: [PATCH] fixes #1131 (#1132) * fixes #1131 --- CHANGELOG_UNRELEASED.md | 5 ++- theories/derive.v | 4 +-- theories/lebesgue_measure.v | 9 ++---- theories/normedtype.v | 62 ++++++++++++++++++------------------- theories/topology.v | 18 ++++++----- 5 files changed, 49 insertions(+), 49 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 89e2e400b..fdadcf05a 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -155,7 +155,10 @@ + `sigma_finite_measure` instance on product measure `\x` ### Changed - + +- 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 6edda28fa..e26f43103 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -682,7 +682,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 /continuous_at linear0 => /(_ _ (nbhsx_ballx 0 1%:pos)). +move=> /(_ 0); rewrite /continuous_at 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. @@ -751,7 +751,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 /continuous_at linear0r => /(_ _ (nbhsx_ballx 0 1%:pos)). +move=> /(_ 0); rewrite /continuous_at 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 a29b5398f..a670be30e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1951,7 +1951,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. @@ -2090,9 +2090,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. @@ -2110,8 +2108,7 @@ have badn' : forall k, exists n, mu (E k n) < ((eps/2) / (2 ^ k.+1)%:R)%:E. - by apply: bigcap_measurable => ?. rewrite measure0; 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 66c9dac3e..7b5526635 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -1033,7 +1033,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)). @@ -3180,36 +3180,33 @@ move=> [x y]; have [pE U /= Upinf|] := eqVneq (edist (x, y)) +oo%E. rewrite -ltey -ge0_fin_numE// => efin. rewrite /continuous_at -[edist (x, y)]fineK//; apply: cvg_EFin. by have := edist_fin_open efin; apply: filter_app; near=> w. -move=> U /=; rewrite nbhs_simpl/= -nbhs_ballE. -move=> [] _/posnumP[r] distrU; rewrite nbhs_simpl /=. -have r2p : 0 < r%:num / 4%:R by rewrite divr_gt0// ltr0n. -exists (ball x (r%:num / 4%:R), ball y (r%:num / 4%:R)). - by split => //=; exact: (@nbhsx_ballx _ _ _ (@PosNum _ _ r2p)). -case => a b /= [/ball_sym xar yar]; apply: distrU => /=. -have abxy : (edist (a, b) <= edist (a, x) + edist (x, y) + edist (y, b))%E. - by rewrite -addeA (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle. +apply/cvgrPdist_le => _/posnumP[eps]. +suff: \forall t \near (nbhs x, nbhs y), + `|fine (edist (x, y)) - fine (edist t)| <= eps%:num by []. +rewrite -near2_pair; near=> a b => /=. +have abxy : (edist (a, b) <= edist (x, a) + edist (x, y) + edist (y, b))%E. + rewrite (edist_sym x a) -addeA. + by rewrite (le_trans (@edist_triangle _ x _)) ?lee_add ?edist_triangle. +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; exact: nbhsx_ballx. +have ybfin : edist (y, b) \is a fin_num. + by apply/edist_finP; exists 1 =>//; near: b; exact: nbhsx_ballx. have abfin : edist (a, b) \is a fin_num. - rewrite ge0_fin_numE// (le_lt_trans abxy)//. - by apply: lte_add_pinfty; [apply: lte_add_pinfty|]; - rewrite -ge0_fin_numE //; apply/edist_finP; exists (r%:num / 4%:R). -have xyabfin : `|edist (x, y) - edist (a, b)|%E \is a fin_num. - by rewrite abse_fin_num fin_numB abfin efin. -have daxr : edist (a, x) \is a fin_num by apply/edist_finP; exists (r%:num / 4). -have dybr : edist (y, b) \is a fin_num by apply/edist_finP; exists (r%:num / 4). -rewrite /ball/= -fineB// -fine_abse ?fin_numB ?abfin ?efin//. -rewrite (@le_lt_trans _ _ (fine (edist (a, x) + edist (y, b))))//. - rewrite fine_le// ?fin_numD ?daxr ?dybr//. - have [xyab|xyab] := leP (edist (a, b)) (edist (x, y)). - rewrite gee0_abs ?subre_ge0// lee_subl_addr//. - rewrite (le_trans (@edist_triangle _ a _))// (edist_sym a x) -addeA. - by rewrite lee_add// addeC (edist_sym y) edist_triangle. - rewrite lte0_abs ?subre_lt0// oppeB ?fin_num_adde_defr// addeC. - by rewrite lee_subl_addr// addeAC. -rewrite fineD // [_%:num]splitr. -have r42 : r%:num / 4 < r%:num / 2. - by rewrite ltr_pM2l// ltf_pV2 ?posrE ?ltr0n// ltr_nat. -by apply: ltrD; rewrite (le_lt_trans _ r42)// -lee_fin fineK // edist_fin. -Unshelve. end_near. Qed. + 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 + by rewrite fin_numB abfin efin. +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]; 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//. +by rewrite addeC lee_subl_addr// addeAC. +Unshelve. all: end_near. Qed. Lemma edist_closeP x y : close x y <-> edist (x, y) = 0%E. Proof. @@ -3297,7 +3294,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. @@ -4644,7 +4641,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 df5e6d2a6..e34adb129 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5033,13 +5033,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: ball_triangle_subproof. 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. @@ -5054,8 +5054,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). @@ -5113,6 +5112,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). @@ -5707,10 +5709,10 @@ 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. +by rewrite -mulr2n -(mulr_natr (_ / _) 2) divfK// => /ltW. Qed. Section RestrictedUniformTopology.