diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5ee0ae5bbd..4991a2ebac 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,6 +88,15 @@ + lemma `open_subball_rat` + fact `isolated_rat_ball` + lemma `countable_isolated` +- in `normed_module.v`: + + lemma `limit_point_setD` + +- in `reals.v`: + + lemma `nat_has_minimum` + +- in `sequences.v`: + + lemma `cluster_eventuallyP` + + lemmas `cluster_eventually_cvg`, `limit_point_cluster_eventually` ### Changed diff --git a/reals/reals.v b/reals/reals.v index 842399f50b..fee962db81 100644 --- a/reals/reals.v +++ b/reals/reals.v @@ -656,6 +656,18 @@ rewrite (le_trans _ (lbBi _ Bk)) //. by move/negP : i1x; rewrite -ltNge ltzD1. Qed. +Lemma nat_has_minimum (A : set nat) : A !=set0 -> + exists j, A j /\ forall k, A k -> (j <= k)%N. +Proof. +move=> A0. +pose B : set int := [set x%:~R | x in A]. +have B0 : B !=set0 by apply: image_nonempty. +have: lbound B 0 by move=> _ [b0 Bb0 <-]; rewrite ler0z. +move/(int_lbound_has_minimum B0) => [_ [[i Ai <-]]] Bi. +exists i; split=> // k Bk. +by have := Bi k%:~R; rewrite ler_int; apply; exists k. +Qed. + Section rat_in_itvoo. Let bound_div (R : archiRealFieldType) (x y : R) : nat := diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 61055e4269..e938cb24a2 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -1096,6 +1096,14 @@ move=> p q _ _ /=; apply: contraPP => /eqP. by rewrite neq_lt => /orP[] /arv /[swap] ->; rewrite ltxx. Qed. +Lemma limit_point_setD {R : archiRealFieldType} (A V : set R) a : + finite_set V -> limit_point A a -> limit_point (A `\` V) a. +Proof. +move=> finV /limit_point_infinite_setP aA. +apply/limit_point_infinite_setP => U aU. +by rewrite setIDA; apply: infinite_setD => //; exact: aA. +Qed. + Lemma EFin_lim (R : realFieldType) (f : nat -> R) : cvgn f -> limn (EFin \o f) = (limn f)%:E. Proof. diff --git a/theories/sequences.v b/theories/sequences.v index 4283d85cb1..1140cf3bff 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -2671,6 +2671,180 @@ apply: nondecreasing_cvgn_le; last exact: is_cvg_geometric_series. by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0. Qed. +(* adherence values of a sequence *) +Lemma cluster_eventuallyP {R : realFieldType} (u_ : R^nat) (a : R) : + cluster (u_ @ \oo) a <-> + forall (e : R) n, e > 0 -> exists2 p, (p >= n)%N & `|a - u_ p| <= e. +Proof. +split => [/= uya e n e0|u_a /= A B [n/= _ nuA] [e/= e0 aeB]]. +- apply/not_exists2P => nuae. + have yuAe : nbhs \oo (u_ @^-1` [set x | `|a - x| > e]). + exists n => // m/= nm; have := nuae m. + by rewrite nm/= => -[//|/negP]; rewrite -ltNge. + have [/= r []] := uya _ _ yuAe (nbhsx_ballx a _ e0). + by rewrite /ball/= => /ltW; rewrite leNgt => /negbTE ->. +- have e20 : 0 < e / 2 by rewrite divr_gt0. + have [p np upae] := u_a _ n e20. + exists (u_ p); split; first exact: nuA. + apply: aeB => /=. + by rewrite (le_lt_trans upae)// gtr_pMr// invf_lt1// ltr1n. +Qed. + +Section cluster_eventually_cvg. +Context {R : realType}. +Variables (u_ : R^nat) (a : R). + +(* We build a sequence of increasing positive indices N_k s.t. + |u_N_k - a| <= 1/k where N_k is the smallest natural number of the set + A(N, k) defined below. *) + +Let A N k := [set j | (j > N)%N /\ `|a - u_ j| <= k.+1%:R^-1]. + +Let elt_prop Nk := + [/\ `|a - u_ Nk.1| <= Nk.2%:R^-1, A Nk.1 Nk.2 !=set0 & (0 < Nk.2)%N]. + +Let elt_type := {x : nat * nat | elt_prop x}. + +Let N_ (x : elt_type) := (proj1_sig x).1. + +Let idx_ (x : elt_type) := (proj1_sig x).2. + +Let N_idx x : `|a - u_ (N_ x)| <= (idx_ x)%:R^-1. +Proof. by move: x => [[? ?]] []. Qed. + +Let A_nonempty x : A (N_ x) (idx_ x) !=set0. +Proof. by move: x => [[? ?]] []. Qed. + +Let elt_rel i j := [/\ idx_ j = (idx_ i).+1, + (N_ j > N_ i)%N & N_ j = proj1_sig (cid (nat_has_minimum (A_nonempty i)))]. + +Let N_incr v k p : (forall n, elt_rel (v n) (v n.+1)) -> + (k < p)%N -> (N_ (v k) < N_ (v p))%N. +Proof. +move=> vrel kp. +have {}Nv n : (N_ (v n) < N_ (v n.+1))%O by have [_] := vrel n. +by move/increasing_seqP/leqW_mono : Nv => ->. +Qed. + +Let idx_incr v n : (forall n, elt_rel (v n) (v n.+1)) -> (n <= idx_ (v n))%N. +Proof. +by move=> vrel; elim: n => // n /leq_ltn_trans; apply; have [->] := vrel n. +Qed. + +Let cluster_eventually_cvg_direct : cluster (u_ @ \oo) a -> + exists2 f : nat -> nat, increasing_seq f & u_ \o f @ \oo --> a. +Proof. +move=> /cluster_eventuallyP u_a. +have [N0 N01] : {N0 | `| a - u_ N0 | <= 1^-1}. + by move: u_a => /(_ 1 1 ltr01)/cid2[N1 _] N1a1; exists N1; rewrite invr1. +have A0 : A N0 1 !=set0. + move: u_a => /(_ 2^-1 N0.+1). + by rewrite invr_gt0// ltr0n => /(_ isT)[j N0j j1]; exists j. +have [v [v0 vrel]] : {v : nat -> elt_type | + v 0 = exist elt_prop (N0, 1) (And3 N01 A0 isT) /\ + forall n, elt_rel (v n) (v n.+1) }. + apply: dependent_choice => // -[[N i] /=] [uNi ANi0 i0]. + pose M := proj1_sig (cid (nat_has_minimum ANi0)). + have Mi1 : `|a - u_ M| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. + have AMi1 : A M i.+1 !=set0. + move: u_a => /(_ i.+2%:R^-1 M.+1). + by rewrite invr_gt0// ltr0n => /(_ isT)/cid2[m nm um]; exists m. + exists (exist elt_prop (M, i.+1) (And3 Mi1 AMi1 isT)). + rewrite /elt_rel/= /N_/=; split; first exact. + - by rewrite /M; case: cid => // x [[]]. + - rewrite /M; case: cid => // x [/= ANix ANi]. + case: cid => //= y [/ANi xy] /(_ _ ANix) yx. + by apply/eqP; rewrite eq_le leEnat xy yx. +exists (N_ \o v \o S). + by apply/increasing_seqP => n; exact: N_incr. +apply/subr_cvg0/cvgrPdist_le => /= e e0; near=> n. +rewrite sub0r normrN distrC (le_trans (N_idx (v n.+1)))//. +rewrite invf_ple ?posrE//; last by rewrite ltr0n; case: (v n.+1) => -[? ?] []. +rewrite (@le_trans _ _ n.+1%:R)//; last by rewrite ler_nat idx_incr. +by rewrite -nat1r -lerBlDl; near: n; exact: nbhs_infty_ger. +Unshelve. all: end_near. Qed. + +Lemma cluster_eventually_cvg : cluster (u_ @ \oo) a <-> + exists2 f : nat -> nat, increasing_seq f & (u_ \o f @ \oo --> a). +Proof. +split => // -[f incrf] /cvgrPdist_le/= auf. +apply/cluster_eventuallyP => e n e0; move: auf. +move=> /(_ _ e0)[N _ {}Nauf]. +exists (f (n + N)); last by rewrite Nauf//= leq_addl. +rewrite (@leq_trans (f n))//. + elim: n => // n; rewrite -ltnS => /leq_trans; apply. + by move/increasing_seqP : incrf; exact. +by rewrite -leEnat incrf leq_addr. +Qed. + +Lemma limit_point_cluster_eventually : + limit_point (range u_) a -> cluster (u_ @ \oo) a. +Proof. +pose U := range u_. +pose V i := [set u_ k | k in `I_i]. +have finV i : finite_set (V i) by exact/finite_image/finite_II. +(* we pick up elements u_N_k from the following set: *) +pose aU k := `]a - k.+1%:R^-1, a + k.+1%:R^-1[ `&` ((U `\` V k) `\ a). +move=> u_a. +have aU0 k : aU k !=set0. + have /(limit_pointP _ _).1 [a_ [au a_a]] := limit_point_setD (finV k) u_a. + move/cvgrPdist_lt => /(_ k.+1%:R^-1). + rewrite invr_gt0 ltr0n => /(_ isT)[N _ a_cvg]. + exists (a_ N); split; first by rewrite /= in_itv/= -ltr_distlC a_cvg/=. + split; last exact/eqP. + split; first by have /au[] := imageT a_ N. + by case => x xk uxaN; have /au[_] := imageT a_ N; apply => /=; exists x. +have idx_aU k : exists N1, u_ N1 \in aU k. + have [/= y [/= a1y [[[m _ umy] Uny] ya]]] := aU0 k. + exists m; rewrite inE /aU umy; split => //=; split => //; split => //. + by exists m. +have [N0 N01] : {N0 | `| a - u_ N0 | <= 1^-1}. + apply/cid; have [a_ [au a_a]] := (limit_pointP _ _).1 u_a. + move/cvgrPdist_le => /(_ _ ltr01)[N _] /(_ _ (leqnn N)) aaN1. + have /au[x _ uxaN] := imageT a_ N. + by exists x; rewrite uxaN invr1. +have A0 : A N0 1 !=set0. + have [N1] := idx_aU N0.+1. + rewrite inE => -[/= uN1 [[[x _ uxuN1] /= VN0N1] uN1_a]]. + exists x; split. + by rewrite ltnNge; apply/negP => xN0; apply: VN0N1; exists x. + move: uN1; rewrite in_itv/= -ltr_distlC uxuN1 distrC => /ltW/le_trans; apply. + by rewrite lef_pV2 ?posrE// ler_nat. +have [v [v0 vrel]] : {v : nat -> elt_type | + v 0%N = exist elt_prop (N0, 1) (And3 N01 A0 isT) /\ + forall n, elt_rel (v n) (v n.+1) }. + apply: dependent_choice => // -[[N i] /=] [uNi ANi0 i0]. + pose M := proj1_sig (cid (nat_has_minimum ANi0)). + have M0 : (0 < M)%N. + by rewrite /M; case: cid => //= x [[+ _] _]; exact: leq_trans. + have Mi1 : `|a - u_ M| <= i.+1%:R^-1 by rewrite /M; case: cid => /= x [[]]. + have AMi1 : A M i.+1 !=set0. + have [N1] := idx_aU (maxn i.+1 M.+1). + rewrite inE => -[/= uN1 [[[x _ uxuN2] /= Vi1M1] uN1_a]]. + have Mx : (M < x)%N. + rewrite ltnNge; apply/negP => xM. + by apply: Vi1M1; exists x => //; rewrite /(`I_ _) leq_max !ltnS xM orbT. + exists x; split => //. + move: uN1; rewrite in_itv -ltr_distlC uxuN2 distrC => /ltW/le_trans; apply. + by rewrite lef_pV2 ?posrE// ler_nat ltnS leq_max ltnSn. + exists (exist elt_prop (M, i.+1) (And3 Mi1 AMi1 isT)). + rewrite /elt_rel/= /N_/=; split; first exact. + - by rewrite /M; case: cid => // x [[]]. + - rewrite /M; case: cid => // x [ANix ANi]/=. + case: cid => //= y; rewrite /idx_/= => -[/ANi xy /(_ _ ANix) yx]. + by apply/eqP; rewrite eq_le leEnat xy yx. +apply/cluster_eventually_cvg; exists (N_ \o v). + by apply/increasing_seqP => n; exact: N_incr. +apply/cvgrPdist_le => /= e e0; near=> n. +have := N_idx (v n); rewrite distrC => /le_trans; apply. +rewrite invf_ple//; last first. + by rewrite posrE ltr0n; case: (v n) => [[? ?] []]. +rewrite (@le_trans _ _ n%:R)//; last by rewrite ler_nat idx_incr. +by near: n; exact: nbhs_infty_ger. +Unshelve. all: end_near. Qed. + +End cluster_eventually_cvg. + Section adjacent_cut. Context {R : realType}. Implicit Types L D E : set R.