From 2640fac13237ee92db25cbfb88b50644fc21068a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 14 Dec 2023 19:54:37 +0900 Subject: [PATCH 1/4] isolate the theory of lime_sup --- CHANGELOG_UNRELEASED.md | 27 ++ theories/constructive_ereal.v | 8 + theories/normedtype.v | 10 + theories/realfun.v | 454 +++++++++++++++++++++++++++++++++- theories/topology.v | 4 + 5 files changed, 502 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 98def5d2e..6647d4d79 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -83,6 +83,33 @@ + lemma `maxe_cvg_0_cvg_fin_num` + lemma `maxe_cvg_maxr_cvg` + lemma `maxe_cvg_0_cvg_0` +- in `constructive_ereal.v` + + lemma `lee_subgt0Pr` + +- in `topology.v`: + + lemma `nbhs_dnbhs_neq` + +- in `normedtype.v`: + + lemma `not_near_at_rightP` + +- in `realfun.v`: + + lemma `cvg_at_right_left_dnbhs` + + lemma `cvg_at_rightP` + + lemma `cvg_at_leftP` + + lemma `cvge_at_rightP` + + lemma `lime_sup` + + lemma `lime_inf` + + lemma `lime_supE` + + lemma `lime_infE` + + lemma `lime_infN` + + lemma `lime_supN` + + lemma `lime_sup_ge0` + + lemma `lime_inf_ge0` + + lemma `lime_supD` + + lemma `lime_sup_le` + + lemma `lime_inf_sup` + + lemma `lim_lime_inf` + + lemma `lim_lime_sup` ### Changed diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v index 070dc5075..9905fb342 100644 --- a/theories/constructive_ereal.v +++ b/theories/constructive_ereal.v @@ -3035,6 +3035,14 @@ apply/(iffP idP) => [|]. by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy. Qed. +Lemma lee_subgt0Pr x y : + reflect (forall e, (0 < e)%R -> x - e%:E <= y) (x <= y). +Proof. +apply/(iffP idP) => [xy e|xy]. + by rewrite lee_subl_addr//; move: e; exact/lee_addgt0Pr. +by apply/lee_addgt0Pr => e e0; rewrite -lee_subl_addr// xy. +Qed. + Lemma lee_mul01Pr x y : 0 <= x -> reflect (forall r, (0 < r < 1)%R -> r%:E * x <= y) (x <= y). Proof. diff --git a/theories/normedtype.v b/theories/normedtype.v index 7b871baf9..e60aacb08 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2077,6 +2077,16 @@ Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y. Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt. Unshelve. all: by end_near. Qed. +Lemma not_near_at_rightP T (f : R -> T) (p : R) (P : pred T) : + ~ (\forall x \near p^'+, P (f x)) -> + forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P (f x). +Proof. +move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t. +apply: contrapT; apply: pePf; apply/andP; split. +- by near: t; exact: nbhs_right_gt. +- by near: t; apply: nbhs_right_lt; rewrite ltr_addl. +Unshelve. all: by end_near. Qed. + End at_left_right. #[global] Typeclasses Opaque at_left at_right. Notation "x ^'-" := (at_left x) : classical_set_scope. diff --git a/theories/realfun.v b/theories/realfun.v index b84a816cc..f47a784a4 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -4,7 +4,7 @@ From mathcomp Require Import matrix interval zmodp vector fieldext falgebra. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality. Require Import ereal reals signed topology prodnormedzmodule normedtype derive. -Require Import real_interval. +Require Import sequences real_interval. From HB Require Import structures. (******************************************************************************) @@ -19,6 +19,11 @@ From HB Require Import structures. (* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) (* continuous up to the boundary *) (* *) +(* lime_sup f a == limit superior of the extended real-valued *) +(* function f at a *) +(* lime_inf f a == limit inferior of the extended real-valued *) +(* function f at a *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -80,8 +85,147 @@ apply: near_eq_cvg; near do rewrite subrK; exists M. by rewrite num_real. Unshelve. all: by end_near. Qed. +Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) : + f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> + f x @[x --> p^'] --> l. +Proof. +move=> /cvgrPdist_le fppl /cvgrPdist_le fpnl; apply/cvgrPdist_le => e e0. +have {fppl}[a /= a0 fppl] := fppl _ e0; have {fpnl}[b /= b0 fpnl] := fpnl _ e0. +near=> t. +have : t != p by near: t; exact: nbhs_dnbhs_neq. +rewrite neq_lt => /orP[tp|pt]. +- apply: fpnl => //=; near: t. + exists (b / 2) => //=; first by rewrite divr_gt0. + move=> z/= + _ => /lt_le_trans; apply. + by rewrite ler_pdivr_mulr// ler_pmulr// ler1n. +- apply: fppl =>//=; near: t. + exists (a / 2) => //=; first by rewrite divr_gt0. + move=> z/= + _ => /lt_le_trans; apply. + by rewrite ler_pdivr_mulr// ler_pmulr// ler1n. +Unshelve. all: by end_near. Qed. + End fun_cvg_realFieldType. +Section cvgr_fun_cvg_seq. +Context {R : realType}. + +Lemma cvg_at_rightP (f : R -> R) (p l : R) : + f x @[x --> p^'+] --> l <-> + (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_; exact/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_right_gt. + - exfalso; apply: abs. + by near: t; by 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. + +Lemma cvg_at_leftP (f : R -> R) (p l : R) : + f x @[x --> p^'-] --> l <-> + (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. + +End cvgr_fun_cvg_seq. + +Section cvge_fun_cvg_seq. +Context {R : realType}. + +Lemma cvge_at_rightP (f : R -> \bar R) (p l : R) : + f x @[x --> p^'+] --> l%:E <-> + (forall u : R^nat, (forall n, u n > p) /\ u --> p -> + f (u n) @[n --> \oo] --> l%:E). +Proof. +split=> [/fine_cvgP [ffin_num fpl] u [pu up]|h]. + apply/fine_cvgP; split; last by move/cvg_at_rightP : fpl; exact. + have [e /= e0 {}ffin_num] := ffin_num. + move/cvgrPdist_lt : up => /(_ _ e0)[s /= s0 {}up]; near=> t. + by apply: ffin_num => //=; apply: up => /=; near: t; exists s. +suff H : \forall F \near p^'+, f F \is a fin_num. + by apply/fine_cvgP; split => //; apply/cvg_at_rightP => u /h /fine_cvgP[]. +apply: contrapT => /not_near_at_rightP abs. +have invn n : 0 < n.+1%:R^-1 :> R by rewrite invr_gt0. +pose y_ n := sval (cid2 (abs (PosNum (invn n)))). +have py_ k : p < y_ k by rewrite /y_ /sval/=; case: cid2 => //= x /andP[]. +have y_p : y_ --> p. + apply/cvgrPdist_lt => e e0; near=> t. + rewrite ltr0_norm// ?subr_lt0// opprB. + rewrite /y_ /sval/=; case: cid2 => //= x /andP[_ + _]. + rewrite ltr_subl_addr => /lt_le_trans; apply. + rewrite addrC ler_add2r -(invrK e) lef_pinv// ?posrE ?invr_gt0//. + near: t. + exists `|ceil e^-1|%N => // k /= ek. + rewrite (le_trans (ceil_ge _))// (@le_trans _ _ `|ceil e^-1|%:~R)//. + by rewrite ger0_norm// ?ceil_ge0// ?invr_ge0// ltW. + by move: ek;rewrite -(leq_add2r 1) !addn1 -(ltr_nat R) => /ltW. +have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p). +near \oo => n. +have mn : (m <= n)%N by near: n; exists m. +have {mn} := mfy_ _ mn. +rewrite /y_ /sval; case: cid2 => /= x _. +Unshelve. all: by end_near. Qed. + +End cvge_fun_cvg_seq. + Section fun_cvg_realType. Context {R : realType}. @@ -393,6 +537,314 @@ End fun_cvg_ereal. End fun_cvg. +(*Section lim_sup_inf. +Variables (T : choiceType) (X : filteredType T) (R : realType) (f : X -> \bar R). + +Definition limf_sup (F : set (set X)) := + ereal_inf [set ereal_sup [set f x | x in V] | V in F]. + +Definition limf_inf (F : set (set X)) := + ereal_sup [set ereal_inf [set f x | x in V] | V in F]. + +End lim_sup_inf.*) + +Section lime_sup_inf. +Variable R : realType. +Local Open Scope ereal_scope. +Implicit Types (f g : R -> \bar R) (a r s l : R). + +Let sup_ball f a r := ereal_sup [set f x | x in ball a r `\ a]. + +Let sup_ball_le f a r s : (r <= s)%R -> sup_ball f a r <= sup_ball f a s. +Proof. +move=> rs; apply: ub_ereal_sup => /= _ /= [t [rt ta] <-]. +by apply: ereal_sup_ub => /=; exists t => //; split => //; exact: le_ball rt. +Qed. + +Let inf_ball f a r := ereal_inf [set f x | x in ball a r `\ a]. + +Let inf_ball_le f a r s : (s <= r)%R -> inf_ball f a r <= inf_ball f a s. +Proof. +move=> sr; apply: lb_ereal_inf => /= _ /= [t [st ta] <-]. +by apply: ereal_inf_lb => /=; exists t => //; split => //; exact: le_ball st. +Qed. + +Let le_sup_ball f g a : + (forall r, (0 < r)%R -> forall y : R, y != a -> ball a r y -> f y <= g y) -> + \forall r \near 0^'+, sup_ball f a r <= sup_ball g a r. +Proof. +move=> fg; near=> r; apply: ub_ereal_sup => /= _ [s [pas /= /eqP ps]] <-. +apply: (@le_trans _ _ (g s)); first exact: (fg r). +by apply: ereal_sup_ub => /=; exists s => //; split => //; exact/eqP. +Unshelve. all: by end_near. Qed. + +Definition lime_sup f a : \bar R := lim (sup_ball f a e @[e --> 0^'+]). + +Definition lime_inf f a : \bar R := lim (inf_ball f a e @[e --> 0^'+]). + +Lemma lime_supE f a : + lime_sup f a = ereal_inf [set sup_ball f a e | e in `]0, +oo[ ]%R. +Proof. +apply/cvg_lim => //; apply: nondecreasing_at_right_cvge => //. +by move=> x; rewrite in_itv/= andbT => x0 y /sup_ball_le. +Qed. + +Lemma lime_infE f a : + lime_inf f a = ereal_sup [set inf_ball f a e | e in `]0, +oo[ ]%R. +Proof. +apply/cvg_lim => //; apply: nonincreasing_at_right_cvge => //. +by move=> x; rewrite in_itv/= andbT => x0 y /inf_ball_le. +Qed. + +Lemma lime_infN f a : lime_inf (\- f) a = - lime_sup f a. +Proof. +rewrite lime_supE lime_infE /ereal_inf oppeK; congr ereal_sup. +apply/seteqP; split=> [_ /= [r r0] <-|]. + exists (sup_ball f a r); first by exists r. + rewrite /inf_ball /ereal_inf image_comp/= compA. + by rewrite (_ : _ \o -%E = id) // funeqE => x/=; rewrite oppeK. +move=> _ /= [_] [r] r0 <- <-; exists r => //. +rewrite /inf_ball /ereal_inf image_comp compA. + by rewrite (_ : _ \o -%E = id) // funeqE => x/=; rewrite oppeK. +Qed. + +Lemma lime_supN f a : lime_sup (\- f) a = - lime_inf f a. +Proof. +rewrite -eqe_oppLRP -lime_infN; congr (lime_inf _ a). +by apply/funext => x; rewrite oppeK. +Qed. + +Lemma lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a. +Proof. +move=> f0; rewrite lime_supE; apply: lb_ereal_inf => /= x [e /=]. +rewrite in_itv/= andbT => e0 <-{x}; rewrite -(ereal_sup1 0) ereal_sup_le //=. +exists (f (a + e / 2)%R); last by rewrite ereal_sup1 f0. +exists (a + e / 2)%R => //=; split. + rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//. + by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n. +by apply/eqP; rewrite gt_eqF// ltr_spaddr// divr_gt0. +Qed. + +Lemma lime_inf_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_inf f a. +Proof. +move=> f0; apply: lime_ge. + apply: nonincreasing_at_right_is_cvge => //. + by move=> x; rewrite in_itv/= andbT => x0 y /inf_ball_le. +by near=> b; apply: lb_ereal_inf => /= _ [r [abr/= ra]] <-; exact: f0. +Unshelve. all: by end_near. Qed. + +Lemma lime_supD f g a : lime_sup f a +? lime_sup g a -> + lime_sup (f \+ g)%E a <= lime_sup f a + lime_sup g a. +Proof. +move=> fg; rewrite /lime_sup -limeD//; last 2 first. + - apply: nondecreasing_at_right_is_cvge => x. + by rewrite in_itv/= andbT => x0 y /sup_ball_le. + - apply: nondecreasing_at_right_is_cvge => x. + by rewrite in_itv/= andbT => x0 y /sup_ball_le. +apply: lee_lim. +- apply: nondecreasing_at_right_is_cvge => x. + by rewrite in_itv/= andbT => x0 y /sup_ball_le. +- apply: nondecreasing_at_right_is_cvge => x. + by rewrite in_itv/= andbT => x0 y xy; rewrite lee_add//; exact: sup_ball_le. +- near=> a0; apply: ub_ereal_sup => _ /= [a1 [a1ae a1a]] <-. + by apply: lee_add; apply: ereal_sup_ub => /=; exists a1. +Unshelve. all: by end_near. Qed. + +Lemma lime_sup_le f g a : + (forall r, (0 < r)%R -> forall y, y != a -> ball a r y -> f y <= g y) -> + lime_sup f a <= lime_sup g a. +Proof. +move=> fg; apply: lee_lim; last exact: le_sup_ball. +- apply: nondecreasing_at_right_is_cvge => r. + by rewrite in_itv/= andbT => r0 ? /sup_ball_le. +- apply: nondecreasing_at_right_is_cvge => r. + by rewrite in_itv/= andbT => r0 ? /sup_ball_le. +Qed. + +Lemma lime_inf_sup f a : lime_inf f a <= lime_sup f a. +Proof. +apply: lee_lim => //. +- apply: nonincreasing_at_right_is_cvge => r. + by rewrite in_itv/= andbT => r0 s rs; exact: inf_ball_le. +- apply: nondecreasing_at_right_is_cvge => r. + by rewrite in_itv/= andbT => r0 s rs; exact: sup_ball_le. +near=> r. +rewrite ereal_sup_le//. +have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2)%R. + exists (a + r / 2)%R => //; split. + rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//. + by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n. + by apply/eqP; rewrite gt_eqF// ltr_spaddr// divr_gt0. +by exists (f (a + r / 2)%R) => //=; rewrite ereal_inf_lb. +Unshelve. all: by end_near. Qed. + +Local Lemma lim_lime_sup' f a (l : R) : + f r @[r --> a] --> l%:E -> lime_sup f a <= l%:E. +Proof. +move=> fpA; apply/lee_addgt0Pr => e e0; apply: lime_le. + apply: nondecreasing_at_right_is_cvge => x. + by rewrite in_itv/= andbT => x0 y /sup_ball_le. +move/fine_cvg : (fpA) => /cvgrPdist_le fpA1. +move/fcvg_is_fine : (fpA); rewrite near_map => -[d d0] fpA2. +have := fpA1 _ e0 => -[q /= q0] H. +near=> x. +apply: ub_ereal_sup => //= _ [y [pry /= yp <-]]. +have ? : f y \is a fin_num. + apply: fpA2. + rewrite /ball_ /= (lt_le_trans pry)//. + by near: x; exact: nbhs_right_le. +rewrite -lee_subel_addl// -(@fineK _ (f y)) // -EFinB lee_fin. +rewrite (le_trans (ler_norm _))// distrC H// /ball_/= ltr_distlC. +move: pry; rewrite /ball/= ltr_distlC => /andP[pay ypa]. +have xq : (x <= q)%R by near: x; exact: nbhs_right_le. +apply/andP; split. + by rewrite (le_lt_trans _ pay)// ler_sub. +by rewrite (lt_le_trans ypa)// ler_add2l. +Unshelve. all: by end_near. +Qed. + +Local Lemma lim_lime_inf' f a (l : R) : + f r @[r --> a] --> l%:E -> l%:E <= lime_inf f a. +Proof. +move=> fpA; apply/lee_subgt0Pr => e e0; apply: lime_ge. + apply: nonincreasing_at_right_is_cvge => x. + by rewrite in_itv/= andbT => x0 y /inf_ball_le. +move/fine_cvg : (fpA) => /cvgrPdist_le fpA1. +move/fcvg_is_fine : (fpA); rewrite near_map => -[d d0] fpA2. +have := fpA1 _ e0 => -[q /= q0] H. +near=> x. +apply: lb_ereal_inf => //= _ [y [pry /= yp <-]]. +have ? : f y \is a fin_num. + apply: fpA2. + rewrite /ball_ /= (lt_le_trans pry)//. + by near: x; exact: nbhs_right_le. +rewrite -(@fineK _ (f y)) // -EFinB lee_fin ler_subl_addr -ler_subl_addl. +rewrite (le_trans (ler_norm _))// H// /ball_/= ltr_distlC. +move: pry; rewrite /ball/= ltr_distlC => /andP[pay ypa]. +have xq : (x <= q)%R by near: x; exact: nbhs_right_le. +apply/andP; split. + by rewrite (le_lt_trans _ pay)// ler_sub. +by rewrite (lt_le_trans ypa)// ler_add2l. +Unshelve. all: by end_near. +Qed. + +Lemma lim_lime_inf f a (l : R) : + f r @[r --> a] --> l%:E -> lime_inf f a = l%:E. +Proof. +move=> h; apply/eqP; rewrite eq_le. +by rewrite lim_lime_inf'// andbT (le_trans (lime_inf_sup _ _))// lim_lime_sup'. +Qed. + +Lemma lim_lime_sup f a (l : R) : + f r @[r --> a] --> l%:E -> lime_sup f a = l%:E. +Proof. +move=> h; apply/eqP; rewrite eq_le. +by rewrite lim_lime_sup'//= (le_trans _ (lime_inf_sup _ _))// lim_lime_inf'. +Qed. + +Local Lemma lime_supP f a l : + lime_sup f a = l%:E -> forall e : {posnum R}, exists d : {posnum R}, + forall x, (ball a d%:num `\ a) x -> f x < l%:E + e%:num%:E. +Proof. +rewrite lime_supE => fal. +have H (e : {posnum R}) : + exists d : {posnum R}, l%:E <= sup_ball f a d%:num < l%:E + e%:num%:E. + apply: contrapT => /forallNP H. + have : ereal_inf [set sup_ball f a r | r in `]0%R, +oo[] \is a fin_num. + by rewrite fal. + move=> /lb_ereal_inf_adherent-/(_ e%:num ltac:(by []))[y] /=. + case=> r; rewrite in_itv/= andbT => r0 <-{y}. + rewrite ltNge => /negP; apply. + have /negP := H (PosNum r0). + rewrite negb_and => /orP[|]. + rewrite -ltNge => farl. + have : ereal_inf [set sup_ball f a r | r in `]0%R, +oo[] < l%:E. + rewrite (le_lt_trans _ farl)//; apply: ereal_inf_lb => /=; exists r => //. + by rewrite in_itv/= r0. + by rewrite fal ltxx. + by rewrite -leNgt; apply: le_trans; rewrite lee_add2r// fal. +move=> e; have [d /andP[lfp fpe]] := H e. +exists d => r /= [] prd rp. +by rewrite (le_lt_trans _ fpe)//; apply: ereal_sup_ub => /=; exists r. +Qed. + +Local Lemma lime_infP f a l : + lime_inf f a = l%:E -> forall e : {posnum R}, exists d : {posnum R}, + forall x, (ball a d%:num `\ a) x -> l%:E - e%:num%:E < f x. +Proof. +move=> /(congr1 oppe); rewrite -lime_supN => /lime_supP => H e. +have [d {}H] := H e. +by exists d => r /H; rewrite lte_oppl oppeD// EFinN oppeK. +Qed. + +Lemma lime_inf_sup_lim f a l : + lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'+] --> l%:E. +Proof. +move=> supfpl inffpl; apply/cvge_at_rightP => u [pu up]. +have fu : \forall n \near \oo, f (u n) \is a fin_num. + have [dsup Hdsup] := lime_supP supfpl (PosNum ltr01). + have [dinf Hdinf] := lime_infP inffpl (PosNum ltr01). + near=> n; rewrite fin_numE; apply/andP; split. + apply/eqP => fxnoo. + suff : (ball a dinf%:num `\ a) (u n) by move=> /Hdinf; rewrite fxnoo. + split; last by apply/eqP; rewrite gt_eqF. + by near: n; move/cvgrPdist_lt : up; exact. + apply/eqP => fxnoo. + suff : (ball a dsup%:num `\ a) (u n) by move=> /Hdsup; rewrite fxnoo. + split; last by apply/eqP; rewrite gt_eqF. + by near: n; move/cvgrPdist_lt : up; exact. +apply/fine_cvgP; split => /=; first exact: fu. +apply/cvgrPdist_le => _/posnumP[e]. +have [d1 Hd1] : exists d1 : {posnum R}, + l%:E - e%:num%:E <= ereal_inf [set f x | x in ball a d1%:num `\ a]. + have : l%:E - e%:num%:E < lime_inf f a. + by rewrite inffpl lte_subl_addr// lte_addl. + rewrite lime_infE => /ereal_sup_gt[x /= [r]]; rewrite in_itv/= andbT. + by move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW. +have [d2 Hd2] : exists d2 : {posnum R}, + ereal_sup [set f x | x in ball a d2%:num `\ a] <= l%:E + e%:num%:E. + have : lime_sup f a < l%:E + e%:num%:E by rewrite supfpl lte_addl. + rewrite lime_supE => /ereal_inf_lt[x /= [r]]; rewrite in_itv/= andbT. + by move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW. +pose d := minr d1%:num d2%:num. +have d0 : (0 < d)%R by rewrite lt_minr; apply/andP; split => //=. +move/cvgrPdist_lt : up => /(_ _ d0)[m _] {}ucvg. +near=> n. +rewrite /= ler_distlC; apply/andP; split. + rewrite -lee_fin EFinB (le_trans Hd1)//. + rewrite (@le_trans _ _ (ereal_inf [set f x | x in ball a d `\ a]))//. + apply: le_ereal_inf => _/= [r [adr ra] <-]; exists r => //; split => //. + by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx. + apply: ereal_inf_lb => /=; exists (u n). + split; last by apply/eqP; rewrite eq_sym lt_eqF. + by apply: ucvg => //=; near: n; by exists m. + by rewrite fineK//; by near: n. +rewrite -lee_fin EFinD (le_trans _ Hd2)//. +rewrite (@le_trans _ _ (ereal_sup [set f x | x in ball a d `\ a]))//; last first. + apply: le_ereal_sup => z/= [r [adr rp] <-{z}]; exists r => //; split => //. + by rewrite /ball/= (lt_le_trans adr)// /d le_minl lexx orbT. +apply: ereal_sup_ub => /=; exists (u n). + split; last by apply/eqP; rewrite eq_sym lt_eqF. + by apply: ucvg => //=; near: n; exists m. +by rewrite fineK//; near: n. +Unshelve. all: by end_near. Qed. + +Local Lemma lime_supP' f a l : + lime_sup f a = l%:E -> forall (e : {posnum R}) (d : {posnum R}), + exists x, (ball a d%:num `\ a) x /\ l%:E - e%:num%:E < f x. +Proof. +move=> fal. +have H (e d : {posnum R}) : l%:E - e%:num%:E < l%:E <= sup_ball f a d%:num. + apply/andP; split; first by rewrite lte_subl_addr// lte_addl. + rewrite -fal lime_supE; apply: ereal_inf_lb => /=; exists d%:num => //. + by rewrite in_itv//= andbT. +move=> e d; have {H}/andP[] := H e d. +move=> /lt_le_trans => /[apply]. +by move/ereal_sup_gt => [_] /= [r [pdr rp]] <- H; exists r. +Qed. + +End lime_sup_inf. + Section derivable_oo_continuous_bnd. Context {R : numFieldType} {V : normedModType R}. diff --git a/theories/topology.v b/theories/topology.v index 15a804186..53cc2cee7 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -2611,6 +2611,10 @@ Definition dnbhs {T : topologicalType} (x : T) := within (fun y => y != x) (nbhs x). Notation "x ^'" := (dnbhs x) : classical_set_scope. +Lemma nbhs_dnbhs_neq {T : topologicalType} (p : T) : + \forall x \near nbhs p^', x != p. +Proof. exact: withinT. Qed. + Lemma dnbhsE (T : topologicalType) (x : T) : nbhs x = x^' `&` at_point x. Proof. rewrite predeqE => A; split=> [x_A|[x_A Ax]]. From b7b3e2a23bd9567559f82eb32f2a9ab8b302ffae Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 4 Jan 2024 15:41:59 +0900 Subject: [PATCH 2/4] 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 6647d4d79..de55bdcd1 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -111,6 +111,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. From 02e076a90632a36fc235f28aa45e122cf29a0fe3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 4 Jan 2024 19:57:41 +0900 Subject: [PATCH 3/4] generic def of limsup --- CHANGELOG_UNRELEASED.md | 17 ++++ theories/lebesgue_integral.v | 3 +- theories/lebesgue_measure.v | 3 +- theories/normedtype.v | 34 ++++++++ theories/realfun.v | 148 +++++++++++++++-------------------- theories/sequences.v | 78 ++++++++++++------ theories/topology.v | 7 ++ 7 files changed, 179 insertions(+), 111 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index de55bdcd1..a68583d20 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -114,6 +114,19 @@ - in `normedtype.v`: + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP` +- in `topology.v`: + + lemma `dnbhs_ball` + +- in `normedtype.v` + + definitions `limf_esup`, `limf_einf` + + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN` + +- in `sequences.v`: + + lemmas `limn_esup_lim`, `limn_einf_lim` + +- in `realfun.v`: + + lemmas `lime_sup_lim`, `lime_inf_lim` + ### Changed - in `normedtype.v`: @@ -148,6 +161,10 @@ - moved from `topology.v` to `mathcomp_extra.v` + definition `monotonous` +- in `sequences.v`: + + `limn_esup` now defined from `lime_sup` + + `limn_einf` now defined from `limn_esup` + ### Renamed - in `exp.v`: diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index a51e63bf3..d41288538 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2370,7 +2370,8 @@ pose g n := fun x => einfs (f ^~ x) n. have mg := measurable_fun_einfs mf. have g0 n x : D x -> 0 <= g n x. by move=> Dx; apply: lb_ereal_inf => _ [m /= nm <-]; exact: f0. -rewrite monotone_convergence //; last first. +under eq_integral do rewrite limn_einf_lim. +rewrite limn_einf_lim monotone_convergence //; last first. move=> x Dx m n mn /=; apply: le_ereal_inf => _ /= [p /= np <-]. by exists p => //=; rewrite (leq_trans mn). apply: lee_lim. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 40ae266c4..f9e100e11 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1823,7 +1823,7 @@ Proof. move=> mf mD; rewrite (_ : (fun _ => _) = (fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0]%N])). by apply: measurable_fun_einfs => // k; exact: measurable_fun_esups. -rewrite funeqE => t; apply/cvg_lim => //. +rewrite funeqE => t; rewrite limn_esup_lim; apply/cvg_lim => //. rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))). exact: cvg_esups_inf. by congr (ereal_inf [set _ | _ in _]); rewrite predeqE. @@ -1834,6 +1834,7 @@ Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) : (forall x, D x -> f_ ^~ x --> f x) -> measurable_fun D f. Proof. move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x). + rewrite limn_esup_lim. by move=> Dx; have /cvg_lim <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx). apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //. by move=> x; rewrite inE => Dx; rewrite fE. diff --git a/theories/normedtype.v b/theories/normedtype.v index 2375669ba..291ecf17c 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -10,6 +10,11 @@ Require Import ereal reals signed topology prodnormedzmodule. (* *) (* Note that balls in topology.v are not necessarily open, here they are. *) (* *) +(* * Limit superior and inferior: *) +(* limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F *) +(* f has type X -> \bar R. *) +(* F has type set (set X). *) +(* *) (* * Normed Topological Abelian groups: *) (* pseudoMetricNormedZmodType R == interface type for a normed topological *) (* Abelian group equipped with a norm *) @@ -144,6 +149,35 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +Section limf_esup_einf. +Variables (T : choiceType) (X : filteredType T) (R : realType). +Implicit Types (f : X -> \bar R) (F : set (set X)). +Local Open Scope ereal_scope. + +Definition limf_esup f F := ereal_inf [set ereal_sup (f @` V) | V in F]. + +Definition limf_einf f F := - limf_esup (\- f) F. + +Lemma limf_esupE f F : + limf_esup f F = ereal_inf [set ereal_sup (f @` V) | V in F]. +Proof. by []. Qed. + +Lemma limf_einfE f F : + limf_einf f F = ereal_sup [set ereal_inf (f @` V) | V in F]. +Proof. +rewrite /limf_einf limf_esupE /ereal_inf oppeK -[in RHS]image_comp /=. +congr (ereal_sup [set _ | _ in [set ereal_sup _ | _ in _]]). +by under eq_fun do rewrite -image_comp. +Qed. + +Lemma limf_esupN f F : limf_esup (\- f) F = - limf_einf f F. +Proof. by rewrite /limf_einf oppeK. Qed. + +Lemma limf_einfN f F : limf_einf (\- f) F = - limf_esup f F. +Proof. by rewrite /limf_einf; under eq_fun do rewrite oppeK. Qed. + +End limf_esup_einf. + Definition pointed_of_zmodule (R : zmodType) : pointedType := PointedType R 0. Definition filtered_of_normedZmod (K : numDomainType) (R : normedZmodType K) diff --git a/theories/realfun.v b/theories/realfun.v index 9fb711502..13ee3f06a 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -19,10 +19,9 @@ From HB Require Import structures. (* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) (* continuous up to the boundary *) (* *) -(* lime_sup f a == limit superior of the extended real-valued *) -(* function f at a *) -(* lime_inf f a == limit inferior of the extended real-valued *) -(* function f at a *) +(* * Limit superior and inferior for functions: *) +(* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) +(* valued function f at point a *) (* *) (******************************************************************************) @@ -513,22 +512,15 @@ End fun_cvg_ereal. End fun_cvg. -(*Section lim_sup_inf. -Variables (T : choiceType) (X : filteredType T) (R : realType) (f : X -> \bar R). - -Definition limf_sup (F : set (set X)) := - ereal_inf [set ereal_sup [set f x | x in V] | V in F]. - -Definition limf_inf (F : set (set X)) := - ereal_sup [set ereal_inf [set f x | x in V] | V in F]. - -End lim_sup_inf.*) - Section lime_sup_inf. Variable R : realType. Local Open Scope ereal_scope. Implicit Types (f g : R -> \bar R) (a r s l : R). +Definition lime_sup f a : \bar R := limf_esup f a^'. + +Definition lime_inf f a : \bar R := - lime_sup (\- f) a. + Let sup_ball f a r := ereal_sup [set f x | x in ball a r `\ a]. Let sup_ball_le f a r s : (r <= s)%R -> sup_ball f a r <= sup_ball f a s. @@ -537,12 +529,26 @@ move=> rs; apply: ub_ereal_sup => /= _ /= [t [rt ta] <-]. by apply: ereal_sup_ub => /=; exists t => //; split => //; exact: le_ball rt. Qed. -Let inf_ball f a r := ereal_inf [set f x | x in ball a r `\ a]. +Let sup_ball_is_cvg f a : cvg (sup_ball f a e @[e --> 0^'+]). +Proof. +apply: nondecreasing_at_right_is_cvge => x. +by rewrite in_itv/= andbT => x0 y /sup_ball_le. +Qed. + +Let inf_ball f a r := - sup_ball (\- f) a r. + +Let inf_ballE f a r : inf_ball f a r = ereal_inf [set f x | x in ball a r `\ a]. +Proof. +by rewrite /inf_ball /ereal_inf; congr (- _); rewrite /sup_ball -image_comp. +Qed. Let inf_ball_le f a r s : (s <= r)%R -> inf_ball f a r <= inf_ball f a s. +Proof. by move=> sr; rewrite /inf_ball lee_oppl oppeK sup_ball_le. Qed. + +Let inf_ball_is_cvg f a : cvg (inf_ball f a e @[e --> 0^'+]). Proof. -move=> sr; apply: lb_ereal_inf => /= _ /= [t [st ta] <-]. -by apply: ereal_inf_lb => /=; exists t => //; split => //; exact: le_ball st. +apply: nonincreasing_at_right_is_cvge => //. +by move=> x; rewrite in_itv/= andbT => x0 y /inf_ball_le. Qed. Let le_sup_ball f g a : @@ -554,41 +560,41 @@ apply: (@le_trans _ _ (g s)); first exact: (fg r). by apply: ereal_sup_ub => /=; exists s => //; split => //; exact/eqP. Unshelve. all: by end_near. Qed. -Definition lime_sup f a : \bar R := lim (sup_ball f a e @[e --> 0^'+]). +Lemma lime_sup_lim f a : lime_sup f a = lim (sup_ball f a e @[e --> 0^'+]). +Proof. +apply/eqP; rewrite eq_le; apply/andP; split. + apply: lime_ge => //; near=> e; apply: ereal_inf_lb => /=. + by exists (ball a e `\ a) => //=; exact: dnbhs_ball. +apply: lb_ereal_inf => /= _ [A [r /= r0 arA] <-]. +apply: lime_le => //; near=> e. +apply: le_ereal_sup => _ [s [ase /eqP sa] <- /=]. +exists s => //; apply: arA => //=; apply: (lt_le_trans ase). +by near: e; exact: nbhs_right_le. +Unshelve. all: by end_near. Qed. -Definition lime_inf f a : \bar R := lim (inf_ball f a e @[e --> 0^'+]). +Lemma lime_inf_lim f a : lime_inf f a = lim (inf_ball f a e @[e --> 0^'+]). +Proof. +rewrite /lime_inf lime_sup_lim -limeN; last exact: sup_ball_is_cvg. +by rewrite /sup_ball; under eq_fun do rewrite -image_comp. +Qed. Lemma lime_supE f a : lime_sup f a = ereal_inf [set sup_ball f a e | e in `]0, +oo[ ]%R. Proof. -apply/cvg_lim => //; apply: nondecreasing_at_right_cvge => //. -by move=> x; rewrite in_itv/= andbT => x0 y /sup_ball_le. +rewrite lime_sup_lim; apply/cvg_lim => //. +apply: nondecreasing_at_right_cvge => //. +by move=> x; rewrite in_itv/= andbT => x0 y; exact: sup_ball_le. Qed. Lemma lime_infE f a : lime_inf f a = ereal_sup [set inf_ball f a e | e in `]0, +oo[ ]%R. -Proof. -apply/cvg_lim => //; apply: nonincreasing_at_right_cvge => //. -by move=> x; rewrite in_itv/= andbT => x0 y /inf_ball_le. -Qed. +Proof. by rewrite /lime_inf lime_supE /ereal_inf oppeK image_comp. Qed. Lemma lime_infN f a : lime_inf (\- f) a = - lime_sup f a. -Proof. -rewrite lime_supE lime_infE /ereal_inf oppeK; congr ereal_sup. -apply/seteqP; split=> [_ /= [r r0] <-|]. - exists (sup_ball f a r); first by exists r. - rewrite /inf_ball /ereal_inf image_comp/= compA. - by rewrite (_ : _ \o -%E = id) // funeqE => x/=; rewrite oppeK. -move=> _ /= [_] [r] r0 <- <-; exists r => //. -rewrite /inf_ball /ereal_inf image_comp compA. - by rewrite (_ : _ \o -%E = id) // funeqE => x/=; rewrite oppeK. -Qed. +Proof. by rewrite /lime_sup -limf_einfN. Qed. Lemma lime_supN f a : lime_sup (\- f) a = - lime_inf f a. -Proof. -rewrite -eqe_oppLRP -lime_infN; congr (lime_inf _ a). -by apply/funext => x; rewrite oppeK. -Qed. +Proof. by rewrite /lime_inf oppeK. Qed. Lemma lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a. Proof. @@ -603,23 +609,17 @@ Qed. Lemma lime_inf_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_inf f a. Proof. -move=> f0; apply: lime_ge. - apply: nonincreasing_at_right_is_cvge => //. - by move=> x; rewrite in_itv/= andbT => x0 y /inf_ball_le. -by near=> b; apply: lb_ereal_inf => /= _ [r [abr/= ra]] <-; exact: f0. +move=> f0; rewrite lime_inf_lim; apply: lime_ge; first exact: inf_ball_is_cvg. +near=> b; rewrite inf_ballE. +by apply: lb_ereal_inf => /= _ [r [abr/= ra]] <-; exact: f0. Unshelve. all: by end_near. Qed. Lemma lime_supD f g a : lime_sup f a +? lime_sup g a -> lime_sup (f \+ g)%E a <= lime_sup f a + lime_sup g a. Proof. -move=> fg; rewrite /lime_sup -limeD//; last 2 first. - - apply: nondecreasing_at_right_is_cvge => x. - by rewrite in_itv/= andbT => x0 y /sup_ball_le. - - apply: nondecreasing_at_right_is_cvge => x. - by rewrite in_itv/= andbT => x0 y /sup_ball_le. -apply: lee_lim. -- apply: nondecreasing_at_right_is_cvge => x. - by rewrite in_itv/= andbT => x0 y /sup_ball_le. +move=> fg; rewrite !lime_sup_lim -limeD//; last first. + by rewrite -!lime_sup_lim. +apply: lee_lim => //. - apply: nondecreasing_at_right_is_cvge => x. by rewrite in_itv/= andbT => x0 y xy; rewrite lee_add//; exact: sup_ball_le. - near=> a0; apply: ub_ereal_sup => _ /= [a1 [a1ae a1a]] <-. @@ -630,36 +630,27 @@ Lemma lime_sup_le f g a : (forall r, (0 < r)%R -> forall y, y != a -> ball a r y -> f y <= g y) -> lime_sup f a <= lime_sup g a. Proof. -move=> fg; apply: lee_lim; last exact: le_sup_ball. -- apply: nondecreasing_at_right_is_cvge => r. - by rewrite in_itv/= andbT => r0 ? /sup_ball_le. -- apply: nondecreasing_at_right_is_cvge => r. - by rewrite in_itv/= andbT => r0 ? /sup_ball_le. +by move=> fg; rewrite !lime_sup_lim; apply: lee_lim => //; exact: le_sup_ball. Qed. Lemma lime_inf_sup f a : lime_inf f a <= lime_sup f a. Proof. -apply: lee_lim => //. -- apply: nonincreasing_at_right_is_cvge => r. - by rewrite in_itv/= andbT => r0 s rs; exact: inf_ball_le. -- apply: nondecreasing_at_right_is_cvge => r. - by rewrite in_itv/= andbT => r0 s rs; exact: sup_ball_le. +rewrite lime_inf_lim lime_sup_lim; apply: lee_lim => //. near=> r. -rewrite ereal_sup_le//. +rewrite ereal_sup_le//. have ? : exists2 x, ball a r x /\ x <> a & f x = f (a + r / 2)%R. exists (a + r / 2)%R => //; split. rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//. by rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n. by apply/eqP; rewrite gt_eqF// ltr_spaddr// divr_gt0. -by exists (f (a + r / 2)%R) => //=; rewrite ereal_inf_lb. +by exists (f (a + r / 2)%R) => //=; rewrite inf_ballE ereal_inf_lb. Unshelve. all: by end_near. Qed. Local Lemma lim_lime_sup' f a (l : R) : f r @[r --> a] --> l%:E -> lime_sup f a <= l%:E. Proof. -move=> fpA; apply/lee_addgt0Pr => e e0; apply: lime_le. - apply: nondecreasing_at_right_is_cvge => x. - by rewrite in_itv/= andbT => x0 y /sup_ball_le. +move=> fpA; apply/lee_addgt0Pr => e e0; rewrite lime_sup_lim. +apply: lime_le => //. move/fine_cvg : (fpA) => /cvgrPdist_le fpA1. move/fcvg_is_fine : (fpA); rewrite near_map => -[d d0] fpA2. have := fpA1 _ e0 => -[q /= q0] H. @@ -682,13 +673,13 @@ Qed. Local Lemma lim_lime_inf' f a (l : R) : f r @[r --> a] --> l%:E -> l%:E <= lime_inf f a. Proof. -move=> fpA; apply/lee_subgt0Pr => e e0; apply: lime_ge. - apply: nonincreasing_at_right_is_cvge => x. - by rewrite in_itv/= andbT => x0 y /inf_ball_le. +move=> fpA; apply/lee_subgt0Pr => e e0; rewrite lime_inf_lim. +apply: lime_ge => //. move/fine_cvg : (fpA) => /cvgrPdist_le fpA1. move/fcvg_is_fine : (fpA); rewrite near_map => -[d d0] fpA2. have := fpA1 _ e0 => -[q /= q0] H. near=> x. +rewrite inf_ballE. apply: lb_ereal_inf => //= _ [y [pry /= yp <-]]. have ? : f y \is a fin_num. apply: fpA2. @@ -776,7 +767,8 @@ have [d1 Hd1] : exists d1 : {posnum R}, have : l%:E - e%:num%:E < lime_inf f a. by rewrite inffpl lte_subl_addr// lte_addl. rewrite lime_infE => /ereal_sup_gt[x /= [r]]; rewrite in_itv/= andbT. - by move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW. + move=> r0 <-{x} H; exists (PosNum r0); rewrite ltW//. + by rewrite -inf_ballE. have [d2 Hd2] : exists d2 : {posnum R}, ereal_sup [set f x | x in ball a d2%:num `\ a] <= l%:E + e%:num%:E. have : lime_sup f a < l%:E + e%:num%:E by rewrite supfpl lte_addl. @@ -805,20 +797,6 @@ apply: ereal_sup_ub => /=; exists (u n). by rewrite fineK//; near: n. Unshelve. all: by end_near. Qed. -Local Lemma lime_supP' f a l : - lime_sup f a = l%:E -> forall (e : {posnum R}) (d : {posnum R}), - exists x, (ball a d%:num `\ a) x /\ l%:E - e%:num%:E < f x. -Proof. -move=> fal. -have H (e d : {posnum R}) : l%:E - e%:num%:E < l%:E <= sup_ball f a d%:num. - apply/andP; split; first by rewrite lte_subl_addr// lte_addl. - rewrite -fal lime_supE; apply: ereal_inf_lb => /=; exists d%:num => //. - by rewrite in_itv//= andbT. -move=> e d; have {H}/andP[] := H e d. -move=> /lt_le_trans => /[apply]. -by move/ereal_sup_gt => [_] /= [r [pdr rp]] <- H; exists r. -Qed. - End lime_sup_inf. Section derivable_oo_continuous_bnd. diff --git a/theories/sequences.v b/theories/sequences.v index de8d8055a..10e12190a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -69,14 +69,15 @@ Require Import reals ereal signed topology normedtype landau. (* positive) extended numbers use the string "nneseries" (resp. "npeseries")*) (* as part of their identifier *) (* *) -(* * Limit superior and inferior: *) -(* sdrop u n := {u_k | k >= n} *) -(* sups u := [sequence sup (sdrop u n)]_n *) -(* infs u := [sequence inf (sdrop u n)]_n *) -(* limn_{inf,sup} == limit inferior/superior for realType *) -(* esups u := [sequence ereal_sup (sdrop u n)]_n *) -(* einfs u := [sequence ereal_inf (sdrop u n)]_n *) -(* limn_e{inf,sup} == limit inferior/superior for \bar R *) +(* * Limit superior and inferior for sequences: *) +(* sdrop u n := {u_k | k >= n} *) +(* sups u := [sequence sup (sdrop u n)]_n *) +(* infs u := [sequence inf (sdrop u n)]_n *) +(* limn_sup, limn_inf == limit sup/inferior for a sequence of reals *) +(* esups u := [sequence ereal_sup (sdrop u n)]_n *) +(* einfs u := [sequence ereal_inf (sdrop u n)]_n *) +(* limn_esup u, limn_einf == limit sup/inferior for a sequence of *) +(* of extended reals *) (* *) (******************************************************************************) @@ -2579,8 +2580,36 @@ Qed. End esups_einfs. -Definition limn_esup (R : realType) (u : (\bar R)^nat) := lim (esups u). -Definition limn_einf (R : realType) (u : (\bar R)^nat) := lim (einfs u). +Section limn_esup_einf. +Context {R : realType}. +Implicit Type (u : (\bar R)^nat). +Local Open Scope ereal_scope. + +Definition limn_esup u := limf_esup u \oo. + +Definition limn_einf u := - limn_esup (\- u). + +Lemma limn_esup_lim u : limn_esup u = lim (esups u). +Proof. +apply/eqP; rewrite eq_le; apply/andP; split. + apply: lime_ge; first exact: is_cvg_esups. + near=> m; apply: ereal_inf_lb => /=. + by exists [set k | (m <= k)%N] => //=; exists m. +apply: lb_ereal_inf => /= _ [A [r /= r0 rA] <-]. +apply: lime_le; first exact: is_cvg_esups. +near=> m; apply: le_ereal_sup => _ [n /= mn] <-. +exists n => //; apply: rA => //=; apply: leq_trans mn. +by near: m; exists r. +Unshelve. all: by end_near. Qed. + +Lemma limn_einf_lim u : limn_einf u = lim (einfs u). +Proof. +rewrite /limn_einf limn_esup_lim esupsN -limeN//. + by under eq_fun do rewrite oppeK. +by apply: is_cvgeN; exact: is_cvg_einfs. +Qed. + +End limn_esup_einf. Section lim_esup_inf. Local Open Scope ereal_scope. @@ -2590,7 +2619,8 @@ Implicit Types (u v : (\bar R)^nat) (l : \bar R). Lemma limn_einf_shift u l : l \is a fin_num -> limn_einf (fun x => l + u x) = l + limn_einf u. Proof. -move=> lfin; apply/cvg_lim => //; apply: cvg_trans; last first. +move=> lfin; rewrite !limn_einf_lim; apply/cvg_lim => //. +apply: cvg_trans; last first. by apply: (@cvgeD _ \oo _ _ (cst l) (einfs u) _ (lim (einfs u))); [exact: fin_num_adde_defr|exact: cvg_cst|exact: is_cvg_einfs]. suff : einfs (fun n => l + u n) = (fun n => l + einfs u n) by move=> ->. @@ -2611,25 +2641,22 @@ move=> supul ul; have usupu n : l <= u n <= esups u n. suff : esups u --> l. by apply: (@squeeze_cvge _ _ _ _ (cst l)) => //; [exact: nearW|exact: cvg_cst]. apply/cvg_closeP; split; first exact: is_cvg_esups. -rewrite closeE//; apply/eqP; rewrite eq_le supul. +rewrite closeE//; apply/eqP. +rewrite eq_le -[X in X <= _ <= _]limn_esup_lim supul/=. apply: (lime_ge (@is_cvg_esups _ _)); apply: nearW => m. have /le_trans : l <= einfs u m by apply: lb_ereal_inf => _ [p /= pm] <-. by apply; exact: einfs_le_esups. Qed. Lemma limn_einfN u : limn_einf (-%E \o u) = - limn_esup u. -Proof. -by rewrite /limn_einf einfsN /limn_esup limeN //; exact/is_cvg_esups. -Qed. +Proof. by rewrite /limn_esup -limf_einfN. Qed. Lemma limn_esupN u : limn_esup (-%E \o u) = - limn_einf u. -Proof. -apply/eqP; rewrite -eqe_oppLR -limn_einfN /=. -by rewrite (_ : _ \o _ = u) // funeqE => n /=; rewrite oppeK. -Qed. +Proof. by rewrite /limn_einf oppeK. Qed. Lemma limn_einf_sup u : limn_einf u <= limn_esup u. Proof. +rewrite limn_esup_lim limn_einf_lim. apply: lee_lim; [exact/is_cvg_einfs|exact/is_cvg_esups|]. by apply: nearW; exact: einfs_le_esups. Qed. @@ -2639,7 +2666,7 @@ Lemma cvgNy_limn_einf_sup u : u --> -oo -> Proof. move=> uoo; suff: limn_esup u = -oo. by move=> {}uoo; split => //; apply/eqP; rewrite -leeNy_eq -uoo limn_einf_sup. -apply: cvg_lim => //=. apply/cvgeNyPle => M. +rewrite limn_esup_lim; apply: cvg_lim => //=; apply/cvgeNyPle => M. have /cvgeNyPle/(_ M)[m _ uM] := uoo. near=> n; apply: ub_ereal_sup => _ [k /= nk <-]. by apply: uM => /=; rewrite (leq_trans _ nk)//; near: n; exists m. @@ -2648,13 +2675,14 @@ Unshelve. all: by end_near. Qed. Lemma cvgNy_einfs u : u --> -oo -> einfs u --> -oo. Proof. move=> /cvgNy_limn_einf_sup[uoo _]. -by apply/cvg_closeP; split; [exact: is_cvg_einfs|rewrite closeE]. +apply/cvg_closeP; split; [exact: is_cvg_einfs|rewrite closeE//]. +by rewrite -limn_einf_lim. Qed. Lemma cvgNy_esups u : u --> -oo -> esups u --> -oo. Proof. -move=> /cvgNy_limn_einf_sup[_ uoo]. -by apply/cvg_closeP; split; [exact: is_cvg_esups|rewrite closeE]. +move=> /cvgNy_limn_einf_sup[_ uoo]; apply/cvg_closeP. +by split; [exact: is_cvg_esups|rewrite closeE// -limn_esup_lim]. Qed. Lemma cvgy_einfs u : u --> +oo -> einfs u --> +oo. @@ -2700,7 +2728,9 @@ Qed. Lemma cvg_limn_einf_sup u l : u --> l -> (limn_einf u = l) * (limn_esup u = l). Proof. -by move=> ul; split; apply/cvg_lim => //; [apply/cvg_einfs|apply/cvg_esups]. +move=> ul; rewrite limn_esup_lim limn_einf_lim; split. +- by apply/cvg_lim => //; exact/cvg_einfs. +- by apply/cvg_lim => //; exact/cvg_esups. Qed. Lemma is_cvg_limn_einfE u : cvg u -> limn_einf u = lim u. diff --git a/theories/topology.v b/theories/topology.v index 53cc2cee7..b762064ab 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -5152,6 +5152,13 @@ Lemma near_ball (y : M) (eps : {posnum R}) : \forall y' \near y, ball y eps%:num y'. Proof. exact: nbhsx_ballx. Qed. +Lemma dnbhs_ball (a : M) (e : R) : (0 < e)%R -> a^' (ball a e `\ a). +Proof. +move: e => _/posnumP[e]; rewrite /dnbhs /within; near=> r => ra. +split => //=; last exact/eqP. +by near: r; rewrite near_simpl; exact: near_ball. +Unshelve. all: by end_near. Qed. + Lemma fcvg_ballP {F} {FF : Filter F} (y : M) : F --> y <-> forall eps : R, 0 < eps -> \forall y' \near F, ball y eps y'. Proof. by rewrite -filter_fromP !nbhs_simpl /=. Qed. From a6b5a2f5b5d2bce87bda7b133ee73b86fa4f4c85 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 8 Jan 2024 00:05:05 +0900 Subject: [PATCH 4/4] left version of a lemma --- CHANGELOG_UNRELEASED.md | 5 +++++ theories/normedtype.v | 44 ++++++++++++++++++++++++++++++++++------- theories/realfun.v | 22 ++++++++++++++++++++- 3 files changed, 63 insertions(+), 8 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index a68583d20..496ab1bb9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -97,6 +97,7 @@ + lemma `cvg_at_rightP` + lemma `cvg_at_leftP` + lemma `cvge_at_rightP` + + lemma `cvge_at_leftP` + lemma `lime_sup` + lemma `lime_inf` + lemma `lime_supE` @@ -110,9 +111,13 @@ + lemma `lime_inf_sup` + lemma `lim_lime_inf` + lemma `lim_lime_sup` + + lemma `lime_sup_inf_at_right` + + lemma `lime_sup_inf_at_left` - in `normedtype.v`: + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP` + + lemma `dnbhsN` + + lemma `limf_esup_dnbhsN` - in `topology.v`: + lemma `dnbhs_ball` diff --git a/theories/normedtype.v b/theories/normedtype.v index 291ecf17c..d947bd320 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -150,7 +150,7 @@ Local Open Scope classical_set_scope. Local Open Scope ring_scope. Section limf_esup_einf. -Variables (T : choiceType) (X : filteredType T) (R : realType). +Variables (T : choiceType) (X : filteredType T) (R : realFieldType). Implicit Types (f : X -> \bar R) (F : set (set X)). Local Open Scope ereal_scope. @@ -248,6 +248,20 @@ move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y). by split; [rewrite -oppzey opprK|rewrite -opptey opprK]. Qed. +Lemma dnbhsN {R : numFieldType} (r : R) : + (- r)%R^' = (fun A => -%R @` A) @` r^'. +Proof. +apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]]. + exists (-%R @` A). + exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//. + by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC. + rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=. + by rewrite opprK. +exists e => //= x/=; rewrite -opprD normrN => axe xa. +exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=. +by rewrite opprK. +Qed. + Module PseudoMetricNormedZmodule. Section ClassDef. Variable R : numDomainType. @@ -1663,6 +1677,15 @@ End Exports. End numFieldNormedType. Import numFieldNormedType.Exports. +Lemma limf_esup_dnbhsN {R : realType} (f : R -> \bar R) (a : R) : + limf_esup f a^' = limf_esup (fun x => f (- x)%R) (- a)%R^'. +Proof. +rewrite /limf_esup dnbhsN image_comp/=. +congr (ereal_inf [set _ | _ in _]); apply/funext => A /=. +rewrite image_comp/= -compA (_ : _ \o _ = idfun)// funeqE => x/=. +by rewrite opprK. +Qed. + Section NormedModule_numDomainType. Variables (R : numDomainType) (V : normedModType R). @@ -2131,18 +2154,25 @@ move=> r aer ar; rewrite -(opprK r); apply: aeE; last by rewrite -memNE. by rewrite /= opprK -normrN opprD. Qed. +Let fun_predC (T : choiceType) (f : T -> T) (p : pred T) : involutive f -> + [set f x | x in p] = [set x | x in p \o f]. +Proof. +by move=> fi; apply/seteqP; split => _/= [y hy <-]; + exists (f y) => //; rewrite fi. +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. +rewrite /at_right withinN [X in within X _](_ : _ = [set u | u < a])//. +rewrite (@fun_predC _ -%R)/=; last exact: opprK. +by rewrite image_id; under eq_fun do rewrite ltr_oppl 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. +rewrite /at_left withinN [X in within X _](_ : _ = [set u | a < u])//. +rewrite (@fun_predC _ -%R)/=; last exact: opprK. +by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK. Qed. End at_left_right. diff --git a/theories/realfun.v b/theories/realfun.v index 13ee3f06a..0e165d108 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -199,6 +199,18 @@ have {mn} := mfy_ _ mn. rewrite /y_ /sval; case: cid2 => /= x _. Unshelve. all: by end_near. Qed. +Lemma cvge_at_leftP (f : R -> \bar R) (p l : R) : + f x @[x --> p^'-] --> l%:E <-> + (forall u : R^nat, (forall n, u n < p) /\ u --> p -> + f (u n) @[n --> \oo] --> l%:E). +Proof. +apply: (iff_trans (cvg_at_leftNP f p l%:E)). +apply: (iff_trans (cvge_at_rightP _ _ l)); split=> h u [up pu]. +- rewrite (_ : u = \- (\- u))%R; last by apply/funext => ?/=; rewrite opprK. + by apply: h; split; [by move=> n; rewrite ltr_oppl opprK|exact: cvgN]. +- by apply: h; split => [n|]; [rewrite ltr_oppl|move/cvgN : pu; rewrite opprK]. +Qed. + End cvge_fun_cvg_seq. Section fun_cvg_realType. @@ -744,7 +756,7 @@ have [d {}H] := H e. by exists d => r /H; rewrite lte_oppl oppeD// EFinN oppeK. Qed. -Lemma lime_inf_sup_lim f a l : +Lemma lime_sup_inf_at_right f a l : lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'+] --> l%:E. Proof. move=> supfpl inffpl; apply/cvge_at_rightP => u [pu up]. @@ -797,6 +809,14 @@ apply: ereal_sup_ub => /=; exists (u n). by rewrite fineK//; near: n. Unshelve. all: by end_near. Qed. +Lemma lime_sup_inf_at_left f a l : + lime_sup f a = l%:E -> lime_inf f a = l%:E -> f x @[x --> a^'-] --> l%:E. +Proof. +move=> supfal inffal; apply/cvg_at_leftNP/lime_sup_inf_at_right. +- by rewrite /lime_sup -limf_esup_dnbhsN. +- by rewrite /lime_inf /lime_sup -(limf_esup_dnbhsN (-%E \o f)) limf_esupN oppeK. +Qed. + End lime_sup_inf. Section derivable_oo_continuous_bnd.