IndisputableMonolith.NavierStokes.FourierExtraction

   1import Mathlib
   2
   3/-!
   4# Fourier-Space Subsequential Extraction (Proved)
   5
   6Cantor diagonal extraction for bounded sequences in proper metric spaces.
   7All results proved — no sorry, no axiom.
   8
   9## Main result
  10
  11`nat_diagonal_extraction`: Given `f : ℕ → ℕ → X` bounded in a proper space,
  12∃ φ (strictly increasing) and g such that f(φ(n), m) → g(m) for every m.
  13-/
  14
  15namespace IndisputableMonolith.NavierStokes.FourierExtraction
  16
  17open Filter Topology
  18
  19theorem tendsto_comp_strictMono {X : Type*} [TopologicalSpace X]
  20    {f : ℕ → X} {x : X} (hf : Tendsto f atTop (𝓝 x))
  21    {ψ : ℕ → ℕ} (hψ : StrictMono ψ) :
  22    Tendsto (f ∘ ψ) atTop (𝓝 x) :=
  23  hf.comp hψ.tendsto_atTop
  24
  25theorem strictMono_id_le {φ : ℕ → ℕ} (hφ : StrictMono φ) : ∀ n, n ≤ φ n := by
  26  intro n; induction n with
  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. -/
  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
  76  | zero =>
  77    exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.1
  78  | succ k ih =>
  79    rw [CE_succ]; exact ih.comp (LE_strictMono f c R hf k)
  80
  81private theorem LE_conv (m : ℕ) :
  82    Tendsto (fun n => f (CE f c R hf m (LE f c R hf m n)) (m + 1)) atTop
  83      (𝓝 (CL f c R hf (m + 1))) :=
  84  (bounded_subseq_tendsto (fun n => f (CE f c R hf m n) (m + 1)) c R
  85    (fun n => hf (CE f c R hf m n) (m + 1))).choose_spec.choose_spec.2
  86
  87private theorem CE_conv_at : ∀ m, Tendsto (fun n => f (CE f c R hf m n) m)
  88    atTop (𝓝 (CL f c R hf m)) := by
  89  intro m; cases m with
  90  | zero =>
  91    exact (bounded_subseq_tendsto (fun n => f n 0) c R (fun n => hf n 0)).choose_spec.choose_spec.2
  92  | succ k => exact LE_conv f c R hf k
  93
  94private theorem CE_conv_le : ∀ m j, j ≤ m →
  95    Tendsto (fun n => f (CE f c R hf m n) j) atTop (𝓝 (CL f c R hf j)) := by
  96  intro m j hj
  97  induction m with
  98  | zero =>
  99    have hj0 : j = 0 := Nat.le_zero.mp hj
 100    subst hj0; exact CE_conv_at f c R hf 0
 101  | succ k ih =>
 102    rcases eq_or_lt_of_le hj with hjk | hjk
 103    · subst hjk; exact CE_conv_at f c R hf (k + 1)
 104    · rw [CE_succ]
 105      exact tendsto_comp_strictMono (ih (Nat.lt_succ_iff.mp hjk)) (LE_strictMono f c R hf k)
 106
 107/-- Factoring: CE(m+p) = CE(m) ∘ ρ with ρ strictly increasing and ρ(k) ≥ k. -/
 108private theorem CE_factor (m p : ℕ) :
 109    ∃ ρ : ℕ → ℕ, StrictMono ρ ∧ (∀ k, k ≤ ρ k) ∧
 110      ∀ k, CE f c R hf (m + p) k = CE f c R hf m (ρ k) := by
 111  induction p with
 112  | zero => exact ⟨id, strictMono_id, fun k => le_refl k, fun _ => rfl⟩
 113  | succ q ih =>
 114    obtain ⟨ρ, hρ_mono, hρ_ge, hρ_eq⟩ := ih
 115    refine ⟨ρ ∘ LE f c R hf (m + q),
 116      hρ_mono.comp (LE_strictMono f c R hf (m + q)),
 117      fun k => le_trans (strictMono_id_le (LE_strictMono f c R hf (m + q)) k)
 118        (hρ_ge (LE f c R hf (m + q) k)),
 119      fun k => ?_⟩
 120    show CE f c R hf (m + (q + 1)) k = CE f c R hf m ((ρ ∘ LE f c R hf (m + q)) k)
 121    have h1 : m + (q + 1) = (m + q) + 1 := by omega
 122    rw [h1, CE_succ]
 123    simp only [Function.comp_apply]
 124    exact hρ_eq _
 125
 126private noncomputable def D : ℕ → ℕ := fun n => CE f c R hf n n
 127
 128private theorem D_succ_gt (n : ℕ) : D f c R hf n < D f c R hf (n + 1) := by
 129  show CE f c R hf n n < CE f c R hf (n + 1) (n + 1)
 130  rw [CE_succ]
 131  show CE f c R hf n n < CE f c R hf n (LE f c R hf n (n + 1))
 132  exact CE_strictMono f c R hf n
 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
 167