From 31ea75483a931094484e0270b60d1dffd1705c50 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 4 Jan 2024 15:41:59 +0900 Subject: [PATCH] more modular cvg_at_leftP proof Co-authored-by: Zachary Stone --- CHANGELOG_UNRELEASED.md | 3 +++ theories/normedtype.v | 38 ++++++++++++++++++++++++++++++++++++++ theories/realfun.v | 40 ++++++++-------------------------------- 3 files changed, 49 insertions(+), 32 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 607e14f95..2dcf3d137 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -81,6 +81,9 @@ + lemma `lim_lime_inf` + lemma `lim_lime_sup` +- in `normedtype.v`: + + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP` + ### Changed - in `normedtype.v`: diff --git a/theories/normedtype.v b/theories/normedtype.v index e60aacb08..2375669ba 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2087,6 +2087,30 @@ apply: contrapT; apply: pePf; apply/andP; split. - by near: t; apply: nbhs_right_lt; rewrite ltr_addl. Unshelve. all: by end_near. Qed. +Lemma withinN (A : set R) a : + within A (nbhs (- a)) = - x @[x --> within (-%R @` A) (nbhs a)]. +Proof. +rewrite eqEsubset /=; split; move=> E /= [e e0 aeE]; exists e => //. + move=> r are ra; apply: aeE; last by rewrite memNE opprK. + by rewrite /= opprK addrC distrC. +move=> r aer ar; rewrite -(opprK r); apply: aeE; last by rewrite -memNE. +by rewrite /= opprK -normrN opprD. +Qed. + +Lemma at_rightN a : (- a)^'+ = -%R @ a^'-. +Proof. +rewrite /at_right withinN (_ : [set - x | x in _] = (fun u => u < a))//. +apply/seteqP; split=> [x [r /[1!ltr_oppl] ? <-//]|x xa/=]. +by exists (- x); rewrite 1?ltr_oppr ?opprK. +Qed. + +Lemma at_leftN a : (- a)^'- = -%R @ a^'+. +Proof. +rewrite /at_left withinN (_ : [set - x | x in _] = (fun u => a < u))//. +apply/seteqP; split=> [x [r /[1!ltr_oppr] ? <-//]|x xa/=]. +by exists (- x); rewrite 1?ltr_oppr ?opprK. +Qed. + End at_left_right. #[global] Typeclasses Opaque at_left at_right. Notation "x ^'-" := (at_left x) : classical_set_scope. @@ -2098,6 +2122,20 @@ Notation "x ^'+" := (at_right x) : classical_set_scope. #[global] Hint Extern 0 (Filter (nbhs _^'-)) => (apply: at_left_proper_filter) : typeclass_instances. +Lemma cvg_at_leftNP {T : topologicalType} {R : numFieldType} + (f : R -> T) a (l : T) : + f @ a^'- --> l <-> f \o -%R @ (- a)^'+ --> l. +Proof. +by rewrite at_rightN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. +Qed. + +Lemma cvg_at_rightNP {T : topologicalType} {R : numFieldType} + (f : R -> T) a (l : T) : + f @ a^'+ --> l <-> f \o -%R @ (- a)^'- --> l. +Proof. +by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. +Qed. + Section open_itv_subset. Context {R : realType}. Variables (A : set R) (x : R). diff --git a/theories/realfun.v b/theories/realfun.v index f47a784a4..9fb711502 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -152,38 +152,14 @@ Lemma cvg_at_leftP (f : R -> R) (p l : R) : (forall u : R^nat, (forall n, u n < p) /\ (u --> p) -> f (u n) @[n --> \oo] --> l). Proof. -split=> [/cvgrPdist_le fpl u [up /cvgrPdist_lt ucvg]|pfl]. - apply/cvgrPdist_le => e e0. - have [r /= r0 {}fpl] := fpl _ e0; have [s /= s0 {}ucvg] := ucvg _ r0. - near=> t; apply: fpl => //=; apply: ucvg => /=. - by near: t; exists s. -apply: contrapT => fpl; move: pfl; apply/existsNP. -suff: exists2 x : R ^nat, - ((forall k, x k < p) /\ x --> p) & ~ f (x n) @[n --> \oo] --> l. - by move=> [x_] h; exists x_; apply/not_implyP. -have [e He] : exists e : {posnum R}, forall d : {posnum R}, - exists xn : R, [/\ xn < p, `|xn - p| < d%:num & `|f xn - l| >= e%:num]. - apply: contrapT; apply: contra_not fpl => /forallNP h. - apply/cvgrPdist_le => e e0; have /existsNP[d] := h (PosNum e0). - move/forallNP => {}h; near=> t. - have /not_and3P[abs|abs|/negP] := h t. - - by exfalso; apply: abs; near: t; exact: nbhs_left_lt. - - exfalso; apply: abs. - by near: t; exists d%:num => //= z/=; rewrite distrC. - - by rewrite -ltNge distrC => /ltW. -have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0. -exists (fun n => sval (cid (He (PosNum (invn n))))). - split => [k|]; first by rewrite /sval/=; case: cid => x []. - apply/cvgrPdist_lt => r r0; near=> t. - rewrite /sval/=; case: cid => x [px xpt _]. - rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pinv ?posrE ?invr_gt0//. - near: t; exists `|ceil (r^-1)|%N => // s /=. - rewrite -ltnS -(@ltr_nat R) => /ltW; apply: le_trans. - by rewrite natr_absz gtr0_norm ?ceil_gt0 ?invr_gt0// ceil_ge. -move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)). -rewrite /sval/=; case: cid => // x [px xpn]. -by rewrite leNgt distrC => /negP. -Unshelve. all: by end_near. Qed. +apply: (iff_trans (cvg_at_leftNP f p l)). +apply: (iff_trans (cvg_at_rightP _ _ _)). +split=> [pfl u [pu up]|pfl u [pu up]]. + rewrite -(opprK u); apply: pfl. + by split; [move=> k; rewrite ltr_oppr opprK//|exact/cvgNP]. +apply: pfl. +by split; [move=> k; rewrite ltr_oppl//|apply/cvgNP => /=; rewrite opprK]. +Qed. End cvgr_fun_cvg_seq.