From 81969914159f7f0c957e627a54263eae72871744 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Mon, 8 Jan 2024 01:15:02 +0900 Subject: [PATCH] isolate the theory of lime_sup (#1121) * isolate the theory of lime_sup - generic def of limsup --------- Co-authored-by: Zachary Stone --- CHANGELOG_UNRELEASED.md | 52 +++++ theories/constructive_ereal.v | 8 + theories/lebesgue_integral.v | 3 +- theories/lebesgue_measure.v | 3 +- theories/normedtype.v | 112 +++++++++ theories/realfun.v | 428 +++++++++++++++++++++++++++++++++- theories/sequences.v | 78 +++++-- theories/topology.v | 11 + 8 files changed, 668 insertions(+), 27 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 98def5d2e..496ab1bb9 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -83,6 +83,54 @@ + 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 `cvge_at_leftP` + + 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` + + 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` + +- 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 @@ -118,6 +166,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/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/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 45622b50e..f0cdb617e 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 7b871baf9..d947bd320 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 : realFieldType). +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) @@ -214,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. @@ -1629,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). @@ -2077,6 +2134,47 @@ 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. + +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. + +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 [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 [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. #[global] Typeclasses Opaque at_left at_right. Notation "x ^'-" := (at_left x) : classical_set_scope. @@ -2088,6 +2186,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 b84a816cc..0e165d108 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,10 @@ From HB Require Import structures. (* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) (* continuous up to the boundary *) (* *) +(* * 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 *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -80,8 +84,135 @@ 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. +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. + +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. + +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. Context {R : realType}. @@ -393,6 +524,301 @@ End fun_cvg_ereal. End fun_cvg. +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. +Proof. +move=> rs; apply: ub_ereal_sup => /= _ /= [t [rt ta] <-]. +by apply: ereal_sup_ub => /=; exists t => //; split => //; exact: le_ball rt. +Qed. + +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. +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 : + (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. + +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. + +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. +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. 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. by rewrite /lime_sup -limf_einfN. Qed. + +Lemma lime_supN f a : lime_sup (\- f) a = - lime_inf f a. +Proof. by rewrite /lime_inf 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; 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_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]] <-. + 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. +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. +rewrite lime_inf_lim lime_sup_lim; apply: lee_lim => //. +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 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; 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. +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; 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. + 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_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]. +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. + 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. + 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. + +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. Context {R : numFieldType} {V : normedModType R}. 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 15a804186..b762064ab 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]]. @@ -5148,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.