Subsequence Dichotomy

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.exists_subseq_bounded_or_tendsto_atTop (a : ℕ → ℝ) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ((∃ (A : ℝ), ∀ (n : ℕ), a (φ n) ≤ A) ∨ Filter.Tendsto (fun (n : ℕ) => a (φ n)) Filter.atTop Filter.atTop)

Step 1 of the proof of prop:aniso:small: every real sequence a admits a strictly increasing subsequence a ∘ φ along which either the values stay bounded above, or the values tend to +∞. Applied to the ratio r_n / λ_n, this splits the analysis of prop:aniso:small into the case where the ratio stays bounded and the case where it escapes to infinity along a subsequence.

theorem CIV.exists_subseq_tendsto_of_bddAbove (a : ℕ → ℝ) (h0 : ∀ (n : ℕ), 0 ≤ a n) (hA : ∃ (A : ℝ), ∀ (n : ℕ), a n ≤ A) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∃ (L : ℝ), 0 ≤ L ∧ Filter.Tendsto (fun (n : ℕ) => a (φ n)) Filter.atTop (nhds L)

Step 1 continued, the bounded branch: a nonnegative sequence bounded above by some A admits a strictly increasing subsequence converging to a limit L ≥ 0. Applied to the ratio r_n / λ_n in the bounded branch of exists_subseq_bounded_or_tendsto_atTop, this produces the finite limit ratio used in prop:aniso:small.