D_strictMono

formal source

 133    (lt_of_lt_of_le (Nat.lt_succ_of_le le_rfl)
 134      (strictMono_id_le (LE_strictMono f c R hf n) (n + 1)))
 135
 136private theorem D_strictMono : StrictMono (D f c R hf) :=
 137  strictMono_nat_of_lt_succ (fun n => D_succ_gt f c R hf n)
 138
 139private theorem D_converges (m : ℕ) :
 140    Tendsto (fun n => f (D f c R hf n) m) atTop (𝓝 (CL f c R hf m)) := by
 141  rw [Metric.tendsto_atTop]
 142  intro ε hε
 143  have h_base := CE_conv_at f c R hf m
 144  rw [Metric.tendsto_atTop] at h_base
 145  obtain ⟨K, hK⟩ := h_base ε hε
 146  refine ⟨max m K, fun n hn => ?_⟩
 147  have hm : m ≤ n := le_of_max_le_left hn
 148  have hK_le : K ≤ n := le_of_max_le_right hn
 149  obtain ⟨p, rfl⟩ := Nat.exists_eq_add_of_le hm
 150  obtain ⟨ρ, _hρ_mono, hρ_ge, hρ_eq⟩ := CE_factor f c R hf m p
 151  show dist (f (CE f c R hf (m + p) (m + p)) m) (CL f c R hf m) < ε
 152  rw [hρ_eq (m + p)]
 153  exact hK (ρ (m + p)) (le_trans hK_le (hρ_ge (m + p)))
 154
 155end Diagonal
 156
 157/-- **Cantor diagonal extraction** for ℕ-indexed bounded sequences
 158in a proper metric space. Fully proved. -/
 159theorem nat_diagonal_extraction {X : Type*} [MetricSpace X] [ProperSpace X]
 160    (f : ℕ → ℕ → X) (c : X) (R : ℝ)
 161    (hf : ∀ n m, dist (f n m) c ≤ R) :
 162    ∃ (φ : ℕ → ℕ) (g : ℕ → X), StrictMono φ ∧
 163      ∀ m, Tendsto (fun n => f (φ n) m) atTop (𝓝 (g m)) :=
 164  ⟨D f c R hf, CL f c R hf, D_strictMono f c R hf, D_converges f c R hf⟩
 165
 166end IndisputableMonolith.NavierStokes.FourierExtraction