Skip to content

Insert a structure of uniform space #242

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

Merged
CohenCyril merged 7 commits into from
Jul 31, 2020
Merged

Insert a structure of uniform space #242

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
02b0765
Insert a structure of uniform space
drouhling Jul 28, 2020
ceee447
Update documentation
drouhling Jul 28, 2020
e24d851
Update changelog
drouhling Jul 29, 2020
4ff7fd3
Follow naming convention
drouhling Jul 29, 2020
6e260fa
Add missing joins
drouhling Jul 29, 2020
7c96c57
Update uniform_bigO.v
drouhling Jul 29, 2020
be176e2
Replace flim with cvg
drouhling Jul 31, 2020
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
3 changes: 3 additions & 0 deletions theories/classical_sets.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -539,6 +539,9 @@ rewrite predeqE => t; split => [capU|cupU i _].
by rewrite -(setCK (U i)) => CU; apply cupU; exists i.
Qed.

Lemma setMT {A B} : (@setT A) `*` (@setT B) = setT.
Proof. by rewrite predeqE. Qed.

Definition is_subset1 {A} (X : set A) := forall x y, X x -> X y -> x = y.
Definition is_fun {A B} (f : A -> B -> Prop) := Logic.all (is_subset1 \o f).
Definition is_total {A B} (f : A -> B -> Prop) := Logic.all (nonempty \o f).
Expand Down
39 changes: 20 additions & 19 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -170,7 +170,8 @@ move=> /diff_locallyP [dfc]; rewrite -addrA.
rewrite (littleo_bigO_eqo (cst (1 : R^o))); last first.
apply/eqOP; near=> k; rewrite /cst [`|1 : R^o|]normr1 mulr1.
near=> y; rewrite ltW //; near: y; apply/nbhs_normP.
by exists k; [near: k; exists 0; rewrite real0|move=> ? /=; rewrite sub0r normrN].
exists k; first by near: k; exists 0; rewrite real0.
by move=> ? /=; rewrite -ball_normE /= sub0r normrN.
rewrite addfo; first by move=> /eqolim; rewrite cvg_shift add0r.
by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
Grab Existential Variables. all: end_near. Qed.
Expand Down Expand Up @@ -303,15 +304,15 @@ pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: (@cvgD _ _ [topologicalType of R^o]).
rewrite -(scale1r (_ _ v)); apply: cvgZl => /= X [e e0].
rewrite /ball_ /= => eX.
apply/nbhsP; rewrite nbhs_E.
apply/nbhs_ballP.
by exists e => //= x _ x0; apply eX; rewrite mulVr // ?unitfE // subrr normr0.
rewrite /g2.
have [/eqP ->|v0] := boolP (v == 0).
rewrite (_ : (fun _ => _) = cst 0); first exact: cvg_cst.
by rewrite funeqE => ?; rewrite scaler0 /k littleo_lim0 // scaler0.
apply/cvg_distP => e e0.
rewrite nearE /=; apply/nbhsP; rewrite nbhs_E.
have /(littleoP [littleo of k]) /nbhsP[i i0 Hi] : 0 < e / (2 * `|v|).
rewrite nearE /=; apply/nbhs_ballP.
have /(littleoP [littleo of k]) /nbhs_ballP[i i0 Hi] : 0 < e / (2 * `|v|).
by rewrite divr_gt0 // pmulr_rgt0 // normr_gt0.
exists (i / `|v|); first by rewrite divr_gt0 // normr_gt0.
move=> /= j; rewrite /ball /= /ball_ add0r normrN.
Expand Down Expand Up @@ -447,13 +448,13 @@ Proof.
apply/eqoP => _ /posnumP[e].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : U) id of f]].
have := littleoP [littleo of [o_ (0 : V') id of g]].
move=> /(_ (e%:num / k%:num)) /(_ _) /nbhsP [//|_ /posnumP[d] hd].
move=> /(_ (e%:num / k%:num)) /(_ _) /nbhs_ballP [//|_ /posnumP[d] hd].
apply: filter_app; near=> x => leOxkx; apply: le_trans (hd _ _) _; last first.
rewrite -ler_pdivl_mull //; apply: le_trans leOxkx _.
by rewrite invf_div mulrA -[_ / _ * _]mulrA mulVf // mulr1.
rewrite -ball_normE /= distrC subr0 (le_lt_trans leOxkx) //.
rewrite -ltr_pdivl_mull //; near: x; rewrite /= !nbhs_simpl.
apply/nbhsP; exists (k%:num ^-1 * d%:num)=> // x.
apply/nbhs_ballP; exists (k%:num ^-1 * d%:num)=> // x.
by rewrite -ball_normE /= distrC subr0.
Grab Existential Variables. all: end_near. Qed.

Expand All @@ -469,14 +470,14 @@ Lemma compOo_eqo (U V' W' : normedModType R) (f : U -> V')
Proof.
apply/eqoP => _ /posnumP[e].
have /bigO_exP [_ /posnumP[k]] := bigOP [bigO of [O_ (0 : V') id of g]].
move=> /nbhsP [_ /posnumP[d] hd].
move=> /nbhs_ballP [_ /posnumP[d] hd].
have ekgt0 : e%:num / k%:num > 0 by [].
have /(_ _ ekgt0) := littleoP [littleo of [o_ (0 : U) id of f]].
apply: filter_app; near=> x => leoxekx; apply: le_trans (hd _ _) _; last first.
by rewrite -ler_pdivl_mull // mulrA [_^-1 * _]mulrC.
rewrite -ball_normE /= distrC subr0; apply: le_lt_trans leoxekx _.
rewrite -ltr_pdivl_mull //; near: x; rewrite /= nbhs_simpl.
apply/nbhsP; exists ((e%:num / k%:num) ^-1 * d%:num)=> // x.
apply/nbhs_ballP; exists ((e%:num / k%:num) ^-1 * d%:num)=> // x.
by rewrite -ball_normE /= distrC subr0.
Grab Existential Variables. all: end_near. Qed.

Expand All @@ -493,7 +494,7 @@ rewrite funeqE => x; apply/eqP; case: (ler0P `|x|) => [|xn0].
by rewrite normr_le0 => /eqP ->; rewrite linear0.
rewrite -normr_le0 -(mul0r `|x|) -ler_pdivr_mulr //.
apply/ler0_addgt0P => _ /posnumP[e]; rewrite ler_pdivr_mulr //.
have /oid /nbhsP [_ /posnumP[d] dfe] := posnum_gt0 e.
have /oid /nbhs_ballP [_ /posnumP[d] dfe] := posnum_gt0 e.
set k := ((d%:num / 2) / (PosNum xn0)%:num)^-1.
rewrite -{1}(@scalerKV _ _ k _ x) // linearZZ normmZ.
rewrite -ler_pdivl_mull; last by rewrite gtr0_norm.
Expand Down Expand Up @@ -675,8 +676,8 @@ 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 => /(_ _ (nbhs_ball 0 1%:pos)).
move=> /nbhsP [_ /posnumP[e] he]; exists (2 / e%:num) => // x.
move=> /(_ 0); rewrite linear0 => /(_ _ (nbhsx_ballx 0 1%:pos)).
move=> /nbhs_ballP [_ /posnumP[e] he]; exists (2 / e%:num) => // x.
case: (lerP `|x| 0) => [|xn0].
by rewrite normr_le0 => /eqP->; rewrite linear0 !normr0 mulr0.
set k := 2 / e%:num * (PosNum xn0)%:num.
Expand Down Expand Up @@ -744,8 +745,8 @@ 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 => /(_ _ (nbhs_ball 0 1%:pos)).
move=> /nbhsP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v.
move=> /(_ 0); rewrite linear0r => /(_ _ (nbhsx_ballx 0 1%:pos)).
move=> /nbhs_ballP [_ /posnumP[e] he]; exists ((2 / e%:num) ^+2) => // u v.
case: (lerP `|u| 0) => [|un0].
by rewrite normr_le0 => /eqP->; rewrite linear0l !normr0 mulr0 mul0r.
case: (lerP `|v| 0) => [|vn0].
Expand Down Expand Up @@ -780,7 +781,7 @@ rewrite ler_pmul ?pmulr_rge0 //; last by rewrite nng_le_maxr /= lexx orbT.
rewrite -ler_pdivl_mull //.
suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite nng_le_maxr /= lexx.
near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite distrC subr0 => /ltW.
by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite -ball_normE /= distrC subr0 => /ltW.
Grab Existential Variables. all: end_near. Qed.

Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
Expand All @@ -791,8 +792,8 @@ Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
Proof.
move=> fc; split=> [q|].
by apply: (@continuousD _ _ _ (fun q => f p.1 q.2) (fun q => f q.1 p.2));
move=> A /(fc (_.1, _.2)) /= /nbhsP [_ /posnumP[e] fpqe_A];
apply/nbhsP; exists e%:num => // r [??]; exact: (fpqe_A (_.1, _.2)).
move=> A /(fc (_.1, _.2)) /= /nbhs_ballP [_ /posnumP[e] fpqe_A];
apply/nbhs_ballP; exists e%:num => // r [??]; exact: (fpqe_A (_.1, _.2)).
apply/eqaddoE; rewrite funeqE => q /=.
rewrite linearDl !linearDr addrA addrC.
rewrite -[f q.1 _ + _ + _]addrA [f q.1 _ + _]addrC addrA [f q.1 _ + _]addrC.
Expand Down Expand Up @@ -933,7 +934,7 @@ rewrite mulrA mulf_div mulr1.
have hDx_neq0 : h + x != 0.
near: h; rewrite !nbhs_simpl; apply/nbhs_normP.
exists `|x|; first by rewrite normr_gt0.
move=> h /=; rewrite distrC subr0 -subr_gt0 => lthx.
move=> h /=; rewrite -ball_normE /= distrC subr0 -subr_gt0 => lthx.
rewrite -(normr_gt0 (h + x : R^o)) addrC -[h]opprK.
apply: lt_le_trans (ler_dist_dist _ _).
by rewrite ger0_norm normrN //; apply: ltW.
Expand Down Expand Up @@ -1357,7 +1358,7 @@ Proof.
move=> cvfx; apply/Logic.eq_sym.
(* should be inferred *)
have atrF := at_right_proper_filter x.
apply: (@cvg_map_lim _ _ _ (at_right _)) => // A /cvfx /nbhsP [_ /posnumP[e] xe_A].
apply: (@cvg_map_lim _ _ _ (at_right _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
by exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
Qed.

Expand All @@ -1367,7 +1368,7 @@ Proof.
move=> cvfx; apply/Logic.eq_sym.
(* should be inferred *)
have atrF := at_left_proper_filter x.
apply: (@cvg_map_lim _ _ _ (at_left _)) => // A /cvfx /nbhsP [_ /posnumP[e] xe_A].
apply: (@cvg_map_lim _ _ _ (at_left _)) => // A /cvfx /nbhs_ballP [_ /posnumP[e] xe_A].
exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _].
by apply: xe_A => //; rewrite eq_sym.
Qed.
Expand Down
10 changes: 5 additions & 5 deletions theories/landau.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1118,11 +1118,11 @@ Lemma near_shift {K : numDomainType} {R : normedModType K}
(\near x, P x) = (\forall z \near y, (P \o shift (x - y)) z).
Proof.
rewrite propeqE; split=> /= /nbhs_normP [_/posnumP[e] ye];
apply/nbhs_normP; exists e%:num => // t /= et.
apply: ye; rewrite /= !opprD addrA addrACA subrr add0r.
apply/nbhs_normP; exists e%:num => // t; rewrite -ball_normE /= => et.
apply: ye; rewrite -ball_normE /= !opprD addrA addrACA subrr add0r.
by rewrite opprK addrC.
have /= := ye (t - (x - y)); rewrite addrNK; apply.
by rewrite opprB addrCA opprD addrA subrr add0r opprB.
by rewrite -ball_normE /= opprB addrCA opprD addrA subrr add0r opprB.
Qed.

Lemma cvg_shift {T : Type} {K : numDomainType} {R : normedModType K}
Expand Down Expand Up @@ -1157,7 +1157,7 @@ suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|.
near +oo => k; near=> y.
rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivl_mull; last by near: k; exists 0; rewrite real0.
near: y; apply/nbhs_normP.
eexists; last by move=> ?; rewrite /= sub0r normrN; apply.
eexists; last by move=> ?; rewrite -ball_normE /= sub0r normrN; apply.
by rewrite mulr_gt0 // invr_gt0; near: k; exists 0; rewrite real0.
have /nbhs_normP [_/posnumP[d]] := Of1.
rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y.
Expand All @@ -1169,7 +1169,7 @@ rewrite -[X in _ <= X]mulr1 -ler_pdivr_mull ?pmulr_rgt0 //; last by near: k; exi
rewrite -(ler_pmul2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //.
rewrite -normm_s.
have <- : GRing.Scale.op s_law =2 s by rewrite GRing.Scale.opE.
rewrite -linearZ fk //= distrC subr0 normmZ ger0_norm //.
rewrite -linearZ fk //= -ball_normE /= distrC subr0 normmZ ger0_norm //.
rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivr_mulr //; last by near: k; exists 0; rewrite real0.
rewrite mulrC -ltr_pdivr_mulr //; near: k; apply: nbhs_pinfty_gt.
Grab Existential Variables. all: end_near. Qed.
Expand Down
2 changes: 1 addition & 1 deletion theories/misc/uniform_bigO.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,4 +105,4 @@ by apply/sRQ => //; split; [apply/Re1|apply/Re2];
rewrite /AbsRing_ball /= absrB subr0.
Qed.

End UniformBigO.
End UniformBigO.
Loading