  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. -/
  61private noncomputable def LE (m : ℕ) : ℕ → ℕ :=
  62  (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
  63    (fun n => hf (CE f c R hf m n) (m + 1))).choose
  64
  65private theorem CE_zero : CE f c R hf 0 =
  66    (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose := rfl
  67
  68private theorem CE_succ (m : ℕ) : CE f c R hf (m + 1) = CE f c R hf m ∘ LE f c R hf m := rfl
  69
  70private theorem LE_strictMono (m : ℕ) : StrictMono (LE f c R hf m) :=
  71  (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
  72    (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.1
  73
  74private theorem CE_strictMono : ∀ m, StrictMono (CE f c R hf m) := by
  75  intro m; induction m with

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.