left/right lim prop for monotonic fun (#1265)

* left/right lim prop for monotonic fun --------- Co-authored-by: IshiguroYoshihiro <[email protected]>
math-comp · Aug 6, 2024 · 0e46de4 · 0e46de4
1 parent 2362c9b
commit 0e46de4
Show file tree

Hide file tree

Showing 2 changed files with 58 additions and 0 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -122,6 +122,9 @@
   + 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 `realfun.v`:
+  + lemmas `nondecreasing_at_left_at_right`, `nonincreasing_at_left_at_right`
+
 ### Changed
 
 - in `topology.v`:

diff --git 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_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_itvW 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_itvW xrs; exact/ltW.
+  + by apply: subset_itvW yrs; exact/ltW.
+- near=> x; exists (f r) => _ /= [s srx <-]; rewrite ndf//.
+  + 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.
+
+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.