bounded_subseq_tendsto

formal source

  27  | zero => exact Nat.zero_le _
  28  | succ k ih => exact Nat.succ_le_of_lt (lt_of_le_of_lt ih (hφ (Nat.lt_succ_of_le le_rfl)))
  29
  30theorem bounded_subseq_tendsto {X : Type*} [MetricSpace X] [ProperSpace X]
  31    (f : ℕ → X) (c : X) (R : ℝ) (hf : ∀ n, dist (f n) c ≤ R) :
  32    ∃ (φ : ℕ → ℕ) (x : X), StrictMono φ ∧ Tendsto (f ∘ φ) atTop (𝓝 x) := by
  33  by_cases hR : 0 ≤ R
  34  · obtain ⟨x, _, φ, hφ, htend⟩ := (isCompact_closedBall c R).tendsto_subseq
  35      (fun n => Metric.mem_closedBall.mpr (hf n))
  36    exact ⟨φ, x, hφ, htend⟩
  37  · exact absurd (le_trans dist_nonneg (hf 0)) (not_le.mpr (lt_of_not_le hR))
  38
  39section Diagonal
  40
  41variable {X : Type*} [MetricSpace X] [ProperSpace X]
  42variable (f : ℕ → ℕ → X) (c : X) (R : ℝ) (hf : ∀ n m, dist (f n m) c ≤ R)
  43
  44/-- Composed extraction at step m: makes columns 0..m converge. -/
  45private noncomputable def CE : ℕ → (ℕ → ℕ)
  46  | 0 => (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose
  47  | m + 1 =>
  48    let φ := CE m
  49    let ψ := (bounded_subseq_tendsto (fun n => f (φ n) (m + 1)) c R
  50                (fun n => hf (φ n) (m + 1))).choose
  51    φ ∘ ψ
  52
  53/-- Limit at column m. -/
  54private noncomputable def CL : ℕ → X
  55  | 0 => (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose
  56  | m + 1 =>
  57    (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
  58      (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose
  59
  60/-- The "local" extraction at step m+1. -/