adherence value, extracted seq, limit point

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
 

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 :=

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.

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.