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

rewriting posnum #511

Merged
merged 9 commits into from
Mar 5, 2022
Merged

rewriting posnum #511

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
eb99111
Rewriting posnum
CohenCyril Mar 9, 2020
0bfe5fc
Make unify more generic
proux01 Jan 28, 2022
f674c9f
Make 1%:nng work
proux01 Jan 28, 2022
d6355ae
Add =0 to the abstract domain
proux01 Jan 29, 2022
e298fe4
Add sign inference on type as a last resort
proux01 Feb 6, 2022
3d3f380
Add documentation
proux01 Feb 5, 2022
ea83ebc
Generalize min and max
proux01 Jan 30, 2022
c52712b
Generalize morphism lemmas
proux01 Feb 5, 2022
a5c139f
simplifications, global attributes
affeldt-aist Mar 5, 2022
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
1 change: 1 addition & 0 deletions _CoqProject
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ theories/measure.v
theories/lebesgue_integral.v
theories/summability.v
theories/functions.v
theories/signed.v
theories/altreals/xfinmap.v
theories/altreals/discrete.v
theories/altreals/realseq.v
Expand Down
6 changes: 3 additions & 3 deletions theories/Rstruct.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -694,7 +694,7 @@ split=> [fcont e|fcont _/RltP/posnumP[e]]; last first.
by move=> y [_ /RltP yxd]; apply/RltP/xd_fxe; rewrite /= distrC.
have /RltP egt0 := [gt0 of e%:num].
have [_ [/RltP/posnumP[d] dx_fxe]] := fcont e%:num egt0.
exists d%:num => // y xyd; case: (eqVneq x y) => [->|xney].
exists d%:num => //= y xyd; case: (eqVneq x y) => [->|xney].
by rewrite subrr normr0.
apply/RltP/dx_fxe; split; first by split=> //; apply/eqP.
by have /RltP := xyd; rewrite distrC.
Expand All @@ -712,10 +712,10 @@ case: (@cvg_ballP _ _ (f @ x) FF (f x)) => {FF}H1 H2.
(* TODO: in need for lemmas and/or refactoring of already existing lemmas (ball vs. Rabs) *)
split => [{H2} - /H1 {}H1 eps|{H1} H].
- have {H1} [//|_/posnumP[x0] Hx0] := H1 eps%:num.
exists x0%:num => // Hx0' /Hx0 /=.
exists x0%:num => //= Hx0' /Hx0 /=.
by rewrite /= distrC; apply.
- apply H2 => _ /posnumP[eps]; move: (H eps) => {H} [_ /posnumP[x0] Hx0].
exists x0%:num => // y /Hx0 /= {}Hx0.
exists x0%:num => //= y /Hx0 /= {}Hx0.
by rewrite /ball /= distrC.
Qed.

Expand Down
53 changes: 26 additions & 27 deletions theories/derive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ move=> /diff_locallyP [dfc]; rewrite -addrA.
rewrite (littleo_bigO_eqo (cst (1 : R))); last first.
apply/eqOP; near=> k; rewrite /cst [`|1|]normr1 mulr1.
near=> y; rewrite ltW //; near: y; apply/nbhs_normP.
exists k; first by near: k; exists 0; rewrite real0.
exists k; first by near: k; exists 0.
by move=> ? /=; rewrite -ball_normE /= sub0r normrN.
rewrite addfo; first by move=> /eqolim; rewrite cvg_comp_shift add0r.
by apply/eqolim0P; apply: (cvg_trans (dfc 0)); rewrite linear0.
Expand All @@ -187,14 +187,13 @@ Proof.
rewrite /cst /=; have [e /(_ (`|e x|/2) _)/nbhs_singleton /=] := littleo.
rewrite pmulr_lgt0 // [`|1|]normr1 mulr1 [X in X <= _]splitr.
rewrite ger_addr pmulr_lle0 // => /implyP.
case : real_ltgtP; rewrite ?realE ?normrE //=.
by apply/orP; left.
by case : real_ltgtP; rewrite ?realE ?normrE //= lexx.
Qed.

Lemma littleo_lim0 (f : X -> Y) (h : _ -> Z) (x : X) :
f @ x --> (0 : Y) -> [o_x f of h] x = 0.
Proof.
move/eqolim0P => ->; have [k /(_ _ [gt0 of 1])/=] := littleo.
move/eqolim0P => ->; have [k /(_ _ [gt0 of 1 : R])/=] := littleo.
by move=> /nbhs_singleton; rewrite mul1r normm_littleo normr_le0 => /eqP.
Qed.

Expand Down Expand Up @@ -456,7 +455,7 @@ apply: filter_app; near=> x => leOxkx; apply: le_trans (hd _ _) _; last first.
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/nbhs_ballP; exists (k%:num ^-1 * d%:num)=> // x.
apply/nbhs_ballP; exists (k%:num ^-1 * d%:num) => //= x.
by rewrite -ball_normE /= distrC subr0.
Unshelve. all: by end_near. Qed.

Expand All @@ -479,7 +478,7 @@ 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/nbhs_ballP; 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.
Unshelve. all: by end_near. Qed.

Expand All @@ -496,13 +495,13 @@ rewrite funeqE => x; apply/eqP; have [|xn0] := real_le0P (normr_real x).
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 /nbhs_ballP [_ /posnumP[d] dfe] := posnum_gt0 e.
have /oid /nbhs_ballP [_ /posnumP[d] dfe] := !! gt0 e.
set k := ((d%:num / 2) / (PosNum xn0)%:num)^-1.
rewrite -{1}(@scalerKV _ _ k _ x) // linearZZ normmZ.
rewrite -{1}(@scalerKV _ _ k _ x) /k // linearZZ normmZ.
rewrite -ler_pdivl_mull; last by rewrite gtr0_norm.
rewrite mulrCA (@le_trans _ _ (e%:num * `|k^-1 *: x|)) //; last first.
by rewrite ler_pmul // normmZ normfV.
apply dfe.
apply: dfe.
rewrite -ball_normE /ball_/= sub0r normrN normmZ.
rewrite invrK -ltr_pdivl_mulr // ger0_norm // ltr_pdivr_mulr //.
by rewrite -mulrA mulVf ?lt0r_neq0 // mulr1 [X in _ < X]splitr ltr_addl.
Expand Down Expand Up @@ -683,14 +682,14 @@ 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.
set k := 2 / e%:num * (PosNum xn0)%:num.
have kn0 : k != 0 by [].
have kn0 : k != 0 by rewrite /k.
have abskgt0 : `|k| > 0 by rewrite normr_gt0.
rewrite -[x in X in X <= _](scalerKV kn0) linearZZ normmZ -ler_pdivl_mull //.
suff /he : ball 0 e%:num (k^-1 *: x).
rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply.
by rewrite ger0_norm // mulVf.
by rewrite ger0_norm /k // mulVf.
rewrite -ball_normE /= distrC subr0 normmZ.
rewrite normfV ger0_norm // invrM ?unitfE // mulrAC mulVf //.
rewrite normfV ger0_norm /k // invrM ?unitfE // mulrAC mulVf //.
by rewrite invf_div mul1r [X in _ < X]splitr; apply: ltr_spaddr.
Qed.

Expand Down Expand Up @@ -756,13 +755,13 @@ have [|vn0] := real_le0P (normr_real v).
rewrite -[`|u|]/((PosNum un0)%:num) -[`|v|]/((PosNum vn0)%:num).
set ku := 2 / e%:num * (PosNum un0)%:num.
set kv := 2 / e%:num * (PosNum vn0)%:num.
rewrite -[X in f X](@scalerKV _ _ ku) // linearZl_LR normmZ.
rewrite -[X in f X](@scalerKV _ _ ku) /ku // linearZl_LR normmZ.
rewrite gtr0_norm // -ler_pdivl_mull //.
rewrite -[X in f _ X](@scalerKV _ _ kv) // linearZr_LR normmZ.
rewrite -[X in f _ X](@scalerKV _ _ kv) /kv // linearZr_LR normmZ.
rewrite gtr0_norm // -ler_pdivl_mull //.
suff /he : ball 0 e%:num (ku^-1 *: u, kv^-1 *: v).
rewrite -ball_normE /= distrC subr0 => /ltW /le_trans; apply.
rewrite ler_pdivl_mull // mulr1 ler_pdivl_mull //.
rewrite ler_pdivl_mull 1?pmulr_lgt0// mulr1 ler_pdivl_mull 1?pmulr_lgt0//.
by rewrite mulrA [ku * _]mulrAC expr2.
rewrite -ball_normE /= distrC subr0.
have -> : (ku^-1 *: u, kv^-1 *: v) =
Expand All @@ -779,11 +778,11 @@ Lemma bilinear_eqo (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) :
Proof.
move=> fc; have [_ /posnumP[k] fschwarz] := bilinear_schwarz fc.
apply/eqoP=> _ /posnumP[e]; near=> x; rewrite (le_trans (fschwarz _ _))//.
rewrite ler_pmul ?pmulr_rge0 //; last by rewrite nng_le_maxr /= lexx orbT.
rewrite ler_pmul ?pmulr_rge0 //; last by rewrite num_le_maxr /= lexx orbT.
rewrite -ler_pdivl_mull //.
suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite nng_le_maxr /= lexx.
suff : `|x| <= k%:num ^-1 * e%:num by apply: le_trans; rewrite num_le_maxr /= lexx.
near: x; rewrite !near_simpl; apply/nbhs_le_nbhs_norm.
by exists (k%:num ^-1 * e%:num) => // ? /=; rewrite -ball_normE /= distrC subr0 => /ltW.
by exists (k%:num ^-1 * e%:num) => //= ? /=; rewrite -ball_normE /= distrC subr0 => /ltW.
Unshelve. all: by end_near. Qed.

Fact dbilin (U V' W' : normedModType R) (f : {bilinear U -> V' -> W'}) p :
Expand All @@ -795,7 +794,7 @@ 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)) /= /nbhs_ballP [_ /posnumP[e] fpqe_A];
apply/nbhs_ballP; exists e%:num => // r [??]; exact: (fpqe_A (_.1, _.2)).
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 @@ -845,7 +844,7 @@ Lemma eqo_pair (U V' W' : normedModType R) (F : filter_on U)
(f : U -> V') (g : U -> W') :
(fun t => ([o_F id of f] t, [o_F id of g] t)) =o_F id.
Proof.
apply/eqoP => _/posnumP[e]; near=> x; rewrite nng_le_maxl /=.
apply/eqoP => _/posnumP[e]; near=> x; rewrite num_le_maxl /=.
by apply/andP; split; near: x; apply: littleoP.
Unshelve. all: by end_near. Qed.

Expand Down Expand Up @@ -1274,9 +1273,9 @@ have : (fun h => - ((f x)^-1 * (f (h *: v + x))^-1) *:
by apply: cvgM => //; apply: cvgN; rewrite expr2 invfM; apply: cvgM;
[exact: cvg_cst| exact: cvgV].
apply: cvg_trans => A [_/posnumP[e] /= Ae].
move: fn0; apply: filter_app; near=> h => /=.
move=> fhvxn0; have he : ball 0 e%:num (h : R) by near: h; exists e%:num.
have hn0 : h != 0 by near: h; exists e%:num.
move: fn0; apply: filter_app; near=> h => /= fhvxn0.
have he : ball 0 e%:num (h : R) by near: h; exists e%:num => /=.
have hn0 : h != 0 by near: h; exists e%:num => /=.
suff <- :
- ((f x)^-1 * (f (h *: v + x))^-1) *: (h^-1 *: (f (h *: v + x) - f x)) =
h^-1 *: ((f (h *: v + x))^-1 - (f x)^-1) by exact: Ae.
Expand Down Expand Up @@ -1350,7 +1349,7 @@ move=> cvfx; apply/Logic.eq_sym.
(* should be inferred *)
have atrF := at_right_proper_filter x.
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.
by exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
Qed.
Arguments cvg_at_rightE {R V} f x.

Expand All @@ -1361,7 +1360,7 @@ move=> cvfx; apply/Logic.eq_sym.
(* should be inferred *)
have atrF := at_left_proper_filter x.
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 _].
exists e%:num => //= y xe_y; rewrite lt_def => /andP [xney _].
by apply: xe_A => //; rewrite eq_sym.
Qed.
Arguments cvg_at_leftE {R V} f x.
Expand Down Expand Up @@ -1419,7 +1418,7 @@ apply/eqP; rewrite eq_le; apply/andP; split.
move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //.
exact/lt0r_neq0.
near=> h; apply: mulr_ge0_le0.
by rewrite invr_ge0; apply: ltW; near: h; exists 1.
by rewrite invr_ge0; apply: ltW; near: h; exists 1 => /=.
rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
exists (b - c); first by rewrite /= subr_gt0 (itvP cab).
move=> h; rewrite /= distrC subr0 /= in_itv /= -ltr_subr_addr.
Expand All @@ -1432,7 +1431,7 @@ apply: le0r_cvg_map; last first.
move=> A [e egt0 Ae]; exists e => // x xe xgt0; apply: Ae => //.
exact/ltr0_neq0.
near=> h; apply: mulr_le0.
by rewrite invr_le0; apply: ltW; near: h; exists 1.
by rewrite invr_le0; apply: ltW; near: h; exists 1 => /=.
rewrite subr_le0 [_%:A]mulr1; apply: cmax; near: h.
exists (c - a); first by rewrite /= subr_gt0 (itvP cab).
move=> h; rewrite /= distrC subr0.
Expand Down
Loading