From 13800f63df592f81db1050aa98aaf93f755e2264 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 22 Jul 2024 11:41:32 +0900 Subject: [PATCH 1/2] left/right lim prop for monotonic fun Co-authored-by: IshiguroYoshihiro --- CHANGELOG_UNRELEASED.md | 5 ++++ classical/set_interval.v | 7 +++++ theories/realfun.v | 55 ++++++++++++++++++++++++++++++++++++++++ 3 files changed, 67 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1e8e625de..a662bef86 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -121,6 +121,11 @@ `total_order`, `nonempty`, `minimum_of`, `maximum_of`, `well_order`, `chain`, `wo_chain` + lemmas `antisymmetric_wo_chain`, `antisymmetric_well_order`, `wo_chainW`, `wo_chain_reflexive`, `wo_chain_antisymmetric`, `Zorn's_lemma`, `Hausdorff_maximal_principle`, `well_ordering_principle` +- in `set_interval.v`: + + lemma `subset_itv_oo_ccW` + +- in `realfun.v`: + + lemmas `nondecreasing_at_left_at_right`, `nonincreasing_at_left_at_right` ### Changed diff --git a/classical/set_interval.v b/classical/set_interval.v index 098ec28f6..981ba12d8 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -207,6 +207,13 @@ move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->]. by rewrite andbT; split => //; exact/nesym/eqP. Qed. +Lemma subset_itv_oo_ccW x y u v : (u <= x)%O -> (y <= v)%O -> + `]x, y[ `<=` `[u, v]. +Proof. +move=> ux yv; apply: (subset_trans _ (@subset_itv_oo_cc _ _ _ _)) => z/=. +by rewrite !in_itv/= => /andP[? zy]; rewrite (le_lt_trans ux) ?(lt_le_trans zy). +Qed. + End set_itv_porderType. Arguments neitv {d T} _. diff --git a/theories/realfun.v b/theories/realfun.v index 04a8e0fee..cbf421435 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -381,6 +381,61 @@ apply: @nonincreasing_at_right_is_cvgr. by rewrite oppr_itvoo. Qed. +Let nondecreasing_at_right_is_cvgrW f a b r : a < r -> r < b -> + {in `[a, b] &, nondecreasing_fun f} -> cvg (f x @[x --> r^'+]). +Proof. +move=> ar rb ndf H; apply: nondecreasing_at_right_is_cvgr. +- near=> s => x y xrs yrs xy; rewrite ndf//. + + by apply: subset_itv_oo_ccW xrs; exact/ltW. + + by apply: subset_itv_oo_ccW yrs; exact/ltW. +- near=> x; exists (f r) => _ /= [s srx <-]; rewrite ndf//. + + by apply: subset_itv_oo_cc; rewrite in_itv/= ar. + + by apply: subset_itv_oo_ccW srx; exact/ltW. + + by move: srx; rewrite in_itv/= => /andP[/ltW]. +Unshelve. all: by end_near. Qed. + +Let nondecreasing_at_left_is_cvgrW f a b r : a < r -> r < b -> + {in `[a, b] &, nondecreasing_fun f} -> cvg (f x @[x --> r^'-]). +Proof. +move=> ar rb ndf H; apply: nondecreasing_at_left_is_cvgr. +- near=> s => x y xrs yrs xy; rewrite ndf//. + + by apply: subset_itv_oo_ccW xrs; exact/ltW. + + by apply: subset_itv_oo_ccW yrs; exact/ltW. +- near=> x; exists (f r) => _ /= [s srx <-]; rewrite ndf//. + + by apply: subset_itv_oo_ccW srx; exact/ltW. + + by apply: subset_itv_oo_cc; rewrite in_itv/= ar. + + by move: srx; rewrite in_itv/= => /andP[_ /ltW]. +Unshelve. all: by end_near. Qed. + +Lemma nondecreasing_at_left_at_right f a b : + {in `[a, b] &, nondecreasing_fun f} -> + {in `]a, b[, forall r, lim (f x @[x --> r^'-]) <= lim (f x @[x --> r^'+])}. +Proof. +move=> ndf r; rewrite in_itv/= => /andP[ar rb]; apply: limr_ge. + exact: nondecreasing_at_right_is_cvgrW ndf. +near=> x; apply: limr_le; first exact: nondecreasing_at_left_is_cvgrW ndf. +near=> y; rewrite ndf// ?in_itv/=. +- apply/andP; split; first by near: y; apply: nbhs_left_ge. + exact: (le_trans _ (ltW rb)). +- by rewrite (le_trans (ltW ar))/= ltW. +- exact: (@le_trans _ _ r). +Unshelve. all: by end_near. Qed. + +Lemma nonincreasing_at_left_at_right f a b : + {in `[a, b] &, nonincreasing_fun f} -> + {in `]a, b[, forall r, lim (f x @[x --> r^'-]) >= lim (f x @[x --> r^'+])}. +Proof. +move=> nif; have ndNf : {in `[a, b] &, nondecreasing_fun (-%R \o f)}. + by move=> x y xab yab xy /=; rewrite lerNl opprK nif. +move/nondecreasing_at_left_at_right : (ndNf) => H x. +rewrite in_itv/= => /andP[ax xb]; rewrite -[leLHS]opprK lerNl -!limN//. +- by apply: H; rewrite !in_itv/= ax. +- rewrite -(opprK f); apply: is_cvgN. + exact: nondecreasing_at_right_is_cvgrW ndNf. +- rewrite -(opprK f);apply: is_cvgN. + exact: nondecreasing_at_left_is_cvgrW ndNf. +Qed. + End fun_cvg_realType. Arguments nondecreasing_at_right_cvgr {R f a} b. From ff2c2e466d8a92f73f97a6bccb5cf44303f10f4b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 5 Aug 2024 10:04:52 +0900 Subject: [PATCH 2/2] rm redundant lemma --- CHANGELOG_UNRELEASED.md | 2 -- classical/set_interval.v | 7 ------- theories/realfun.v | 12 ++++++------ 3 files changed, 6 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a662bef86..c13070141 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -121,8 +121,6 @@ `total_order`, `nonempty`, `minimum_of`, `maximum_of`, `well_order`, `chain`, `wo_chain` + lemmas `antisymmetric_wo_chain`, `antisymmetric_well_order`, `wo_chainW`, `wo_chain_reflexive`, `wo_chain_antisymmetric`, `Zorn's_lemma`, `Hausdorff_maximal_principle`, `well_ordering_principle` -- in `set_interval.v`: - + lemma `subset_itv_oo_ccW` - in `realfun.v`: + lemmas `nondecreasing_at_left_at_right`, `nonincreasing_at_left_at_right` diff --git a/classical/set_interval.v b/classical/set_interval.v index 981ba12d8..098ec28f6 100644 --- a/classical/set_interval.v +++ b/classical/set_interval.v @@ -207,13 +207,6 @@ move=> /andP[]; rewrite lt_neqAle => /andP[xz zx ->]. by rewrite andbT; split => //; exact/nesym/eqP. Qed. -Lemma subset_itv_oo_ccW x y u v : (u <= x)%O -> (y <= v)%O -> - `]x, y[ `<=` `[u, v]. -Proof. -move=> ux yv; apply: (subset_trans _ (@subset_itv_oo_cc _ _ _ _)) => z/=. -by rewrite !in_itv/= => /andP[? zy]; rewrite (le_lt_trans ux) ?(lt_le_trans zy). -Qed. - End set_itv_porderType. Arguments neitv {d T} _. diff --git a/theories/realfun.v b/theories/realfun.v index cbf421435..d88ffe174 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -386,11 +386,11 @@ Let nondecreasing_at_right_is_cvgrW f a b r : a < r -> r < b -> Proof. move=> ar rb ndf H; apply: nondecreasing_at_right_is_cvgr. - near=> s => x y xrs yrs xy; rewrite ndf//. - + by apply: subset_itv_oo_ccW xrs; exact/ltW. - + by apply: subset_itv_oo_ccW yrs; exact/ltW. + + by apply: subset_itvW xrs; exact/ltW. + + by apply: subset_itvW yrs; exact/ltW. - near=> x; exists (f r) => _ /= [s srx <-]; rewrite ndf//. + by apply: subset_itv_oo_cc; rewrite in_itv/= ar. - + by apply: subset_itv_oo_ccW srx; exact/ltW. + + by apply: subset_itvW srx; exact/ltW. + by move: srx; rewrite in_itv/= => /andP[/ltW]. Unshelve. all: by end_near. Qed. @@ -399,10 +399,10 @@ Let nondecreasing_at_left_is_cvgrW f a b r : a < r -> r < b -> Proof. move=> ar rb ndf H; apply: nondecreasing_at_left_is_cvgr. - near=> s => x y xrs yrs xy; rewrite ndf//. - + by apply: subset_itv_oo_ccW xrs; exact/ltW. - + by apply: subset_itv_oo_ccW yrs; exact/ltW. + + by apply: subset_itvW xrs; exact/ltW. + + by apply: subset_itvW yrs; exact/ltW. - near=> x; exists (f r) => _ /= [s srx <-]; rewrite ndf//. - + by apply: subset_itv_oo_ccW srx; exact/ltW. + + by apply: subset_itvW srx; exact/ltW. + by apply: subset_itv_oo_cc; rewrite in_itv/= ar. + by move: srx; rewrite in_itv/= => /andP[_ /ltW]. Unshelve. all: by end_near. Qed.