adherence value, extracted seq, limit point

CHANGELOG_UNRELEASED.md

@@ -34,6 +34,16 @@
   + definition `cut`
   + lemmas `cut_adjacent`, `infinite_bounded_limit_point_nonempty`
 
+- in `normed_module.v`:
+  + lemma `limit_point_setD`
+
+- in `reals.v`:
+  + lemma `nat_has_minimum`
+
+- in `sequences.v`:
+  + definition `adherence_value`
+  + lemmas `adherence_value_cvg`, `limit_point_adherence_value`
+
 ### Changed
 
 - in `charge.v`:

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 case: A0 => a Aa; exists a%:~R, a.
+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

@@ -57,6 +57,7 @@ From mathcomp Require Import ereal topology tvs normedtype landau.
 (*                             is convergent and its limit is sup u_n         *)
 (*    nonincreasing_cvgn u_ == if u_ is nonincreasing u_ and bound by below   *)
 (*                             then u_ is convergent                          *)
+(*     adherence_value u_ a == a is an adherence value of the sequence u_     *)
 (*             adjacent_seq == adjacent sequences lemma                       *)
 (*                   cesaro == Cesaro's lemma                                 *)
 (* ```                                                                        *)
@@ -2671,6 +2672,163 @@ apply: nondecreasing_cvgn_le; last exact: is_cvg_geometric_series.
 by apply: nondecreasing_series => ? _ /=; rewrite pmulr_lge0 // exprn_gt0.
 Qed.
 
+Definition adherence_value {R : numDomainType} (u_ : R^nat) (a : R) :=
+  forall (e : R) n, e > 0 -> exists2 p, (p >= n)%N & `|u_ p - a| <= e.
+
+Section adherence_value_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 /\ `|u_ j - a| <= k.+1%:R^-1].
+
+Let elt_prop Nk :=
+  [/\ `|u_ Nk.1 - a| <= 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 : `|u_ (N_ x) - a| <= (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 adherence_value_cvg_direct : adherence_value u_ a ->
+  exists2 f : nat -> nat, increasing_seq f & (u_ \o f @ \oo --> a).
+Proof.
+move=> u_a.
+have [N0 N01] : {N0 | `| u_ N0 - a | <= 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 : `|u_ M - a| <= 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 (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 adherence_value_cvg : adherence_value u_ a <->
+  exists2 f : nat -> nat, increasing_seq f & (u_ \o f @ \oo --> a).
+Proof.
+split => // -[f incrf] /cvgrPdist_le/= + e n e0.
+move=> /(_ _ e0)[N _ {}Nauf].
+exists (f (n + N)); last by rewrite distrC 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_adherence_value :
+  limit_point (range u_) a -> adherence_value u_ 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 | `| u_ N0 - a | <= 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 distrC 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 : `|u_ M - a| <= 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/adherence_value_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 adherence_value_cvg.
+
 Section adjacent_cut.
 Context {R : realType}.
 Implicit Types L D E : set R.