Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fixes #1131 #1132

Merged
merged 3 commits into from
Jan 18, 2024
Merged

fixes #1131 #1132

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
34c7bcf
fixes #1131
affeldt-aist Jan 5, 2024
a94cd43
fix changelog
affeldt-aist Jan 17, 2024
5292806
fix
affeldt-aist Jan 17, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 4 additions & 1 deletion CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,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
Expand Down
4 changes: 2 additions & 2 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
9 changes: 3 additions & 6 deletions theories/lebesgue_measure.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand All @@ -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// => ? [? _ []].
Expand Down
13 changes: 7 additions & 6 deletions theories/normedtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)).
Expand Down Expand Up @@ -4043,17 +4043,17 @@ 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
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]; 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//.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down
18 changes: 10 additions & 8 deletions theories/topology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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).
Expand Down Expand Up @@ -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).

Expand Down Expand Up @@ -6252,10 +6254,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.
Expand Down
Loading