IndisputableMonolith.NavierStokes.GalerkinEquicontinuity

   1import Mathlib
   2import IndisputableMonolith.NavierStokes.Galerkin3D
   3
   4/-!
   5# Galerkin Equicontinuity — McShane Extension (Proved)
   6
   7Lipschitz constant for Fourier coefficients + rational approximation
   8+ Lipschitz dense extension via the McShane upper extension.
   9
  10All results proved — no sorry, no axiom.
  11-/
  12
  13namespace IndisputableMonolith.NavierStokes.GalerkinEquicontinuity
  14
  15open Filter Topology
  16
  17noncomputable section
  18
  19def lipschitzConst (ν B kSq_val C_bilin : ℝ) : ℝ :=
  20  ν * kSq_val * B + C_bilin * B ^ 2
  21
  22theorem lipschitzConst_nonneg {ν B kSq_val C_bilin : ℝ}
  23    (hν : 0 ≤ ν) (hB : 0 ≤ B) (hkSq : 0 ≤ kSq_val) (hC : 0 ≤ C_bilin) :
  24    0 ≤ lipschitzConst ν B kSq_val C_bilin := by
  25  unfold lipschitzConst; positivity
  26
  27/-- For any real t and ε > 0, there's a rational q with |t - q| < ε. -/
  28theorem exists_rat_near (t : ℝ) {ε : ℝ} (hε : 0 < ε) :
  29    ∃ q : ℚ, |t - (q : ℝ)| < ε := by
  30  obtain ⟨q, hq1, hq2⟩ := exists_rat_btwn (show t - ε < t + ε by linarith)
  31  exact ⟨q, by rw [abs_lt]; constructor <;> linarith⟩
  32
  33/-- Limit of bounded sequence is in closed ball. -/
  34theorem limit_in_closedBall {X : Type*} [PseudoMetricSpace X]
  35    (f : ℕ → X) (c : X) (R : ℝ) (x : X)
  36    (hf : ∀ n, dist (f n) c ≤ R)
  37    (hx : Tendsto f atTop (𝓝 x)) :
  38    dist x c ≤ R :=
  39  le_of_tendsto (hx.dist tendsto_const_nhds) (Filter.Eventually.of_forall hf)
  40
  41/-!
  42## McShane upper extension
  43
  44g(t) = inf_{q ∈ ℚ} (g_rat(q) + L * |t - q|)
  45
  46This is L-Lipschitz and extends g_rat.
  47-/
  48
  49private theorem mcshane_bddBelow
  50    (g_rat : ℚ → ℝ) (L : ℝ) (hL : 0 ≤ L) (t : ℝ)
  51    (h_g_lip : ∀ q₁ q₂ : ℚ, |g_rat q₁ - g_rat q₂| ≤ L * |(q₁ : ℝ) - q₂|) :
  52    BddBelow (Set.range (fun q : ℚ => g_rat q + L * |t - (q : ℝ)|)) := by
  53  refine ⟨g_rat 0 - L * |t|, ?_⟩
  54  rintro x ⟨q, rfl⟩
  55  have hg := h_g_lip 0 q
  56  -- Triangle: |0 - q| ≤ |t - q| + |t|
  57  have htri : |(0 : ℝ) - (q : ℝ)| ≤ |t - (q : ℝ)| + |t| := by
  58    have h1 := abs_add_le ((0 : ℝ) - t) (t - (q : ℝ))
  59    have h2 : (0 : ℝ) - t + (t - (q : ℝ)) = 0 - (q : ℝ) := by ring
  60    rw [h2] at h1
  61    have h3 : |(0 : ℝ) - t| = |t| := by
  62      have : (0 : ℝ) - t = -t := by ring
  63      rw [this, abs_neg]
  64    linarith
  65  have hmul := mul_le_mul_of_nonneg_left htri hL
  66  have hexp : L * (|t - (q : ℝ)| + |t|) = L * |t - (q : ℝ)| + L * |t| := by ring
  67  have ha : g_rat 0 - g_rat q ≤ L * |(0 : ℝ) - (q : ℝ)| := by
  68    have hg' : |g_rat 0 - g_rat q| ≤ L * |(0 : ℝ) - (q : ℝ)| := by
  69      have := hg; simp only [Rat.cast_zero] at this; exact this
  70    linarith [le_abs_self (g_rat 0 - g_rat q)]
  71  linarith [ha, hmul, hexp]
  72
  73private theorem mcshane_at_rat
  74    (g_rat : ℚ → ℝ) (L : ℝ) (hL : 0 ≤ L) (q₀ : ℚ)
  75    (h_g_lip : ∀ q₁ q₂ : ℚ, |g_rat q₁ - g_rat q₂| ≤ L * |(q₁ : ℝ) - q₂|) :
  76    iInf (fun q : ℚ => g_rat q + L * |(q₀ : ℝ) - (q : ℝ)|) = g_rat q₀ := by
  77  apply le_antisymm
  78  · -- Upper: iInf ≤ value at q₀ (= g_rat q₀ + 0)
  79    apply ciInf_le_of_le (mcshane_bddBelow g_rat L hL q₀ h_g_lip) q₀
  80    simp
  81  · -- Lower: g_rat q₀ ≤ every value
  82    apply le_ciInf
  83    intro q
  84    have h := h_g_lip q₀ q
  85    linarith [le_abs_self (g_rat q₀ - g_rat q)]
  86
  87private theorem mcshane_lipschitz
  88    (g_rat : ℚ → ℝ) (L : ℝ) (hL : 0 ≤ L)
  89    (h_g_lip : ∀ q₁ q₂ : ℚ, |g_rat q₁ - g_rat q₂| ≤ L * |(q₁ : ℝ) - q₂|)
  90    (t₁ t₂ : ℝ) :
  91    |iInf (fun q : ℚ => g_rat q + L * |t₁ - (q : ℝ)|) -
  92     iInf (fun q : ℚ => g_rat q + L * |t₂ - (q : ℝ)|)| ≤ L * |t₁ - t₂| := by
  93  rw [abs_le]
  94  -- Helper: triangle inequality for absolute values
  95  have tri₁₂ : ∀ q : ℚ, |t₂ - (q : ℝ)| ≤ |t₁ - (q : ℝ)| + |t₁ - t₂| := fun q => by
  96    have h := abs_add_le (t₂ - t₁) (t₁ - (q : ℝ))
  97    have : t₂ - t₁ + (t₁ - (q : ℝ)) = t₂ - (q : ℝ) := by ring
  98    rw [this] at h
  99    linarith [abs_sub_comm t₁ t₂]
 100  have tri₂₁ : ∀ q : ℚ, |t₁ - (q : ℝ)| ≤ |t₂ - (q : ℝ)| + |t₁ - t₂| := fun q => by
 101    have h := abs_add_le (t₁ - t₂) (t₂ - (q : ℝ))
 102    have : t₁ - t₂ + (t₂ - (q : ℝ)) = t₁ - (q : ℝ) := by ring
 103    rw [this] at h; linarith
 104  constructor
 105  · -- iInf₁ - iInf₂ ≥ -L|t₁-t₂|, i.e., iInf₂ ≤ iInf₁ + L|t₁-t₂|
 106    suffices h : iInf (fun q : ℚ => g_rat q + L * |t₂ - (q : ℝ)|) ≤
 107                 iInf (fun q : ℚ => g_rat q + L * |t₁ - (q : ℝ)|) + L * |t₁ - t₂| by linarith
 108    rw [← sub_le_iff_le_add]
 109    apply le_ciInf
 110    intro q
 111    have hle := ciInf_le (mcshane_bddBelow g_rat L hL t₂ h_g_lip) q
 112    have hm := mul_le_mul_of_nonneg_left (tri₁₂ q) hL
 113    linarith [show L * (|t₁ - (q : ℝ)| + |t₁ - t₂|) =
 114              L * |t₁ - (q : ℝ)| + L * |t₁ - t₂| from by ring]
 115  · -- iInf₁ - iInf₂ ≤ L|t₁-t₂|, i.e., iInf₁ ≤ iInf₂ + L|t₁-t₂|
 116    suffices h : iInf (fun q : ℚ => g_rat q + L * |t₁ - (q : ℝ)|) ≤
 117                 iInf (fun q : ℚ => g_rat q + L * |t₂ - (q : ℝ)|) + L * |t₁ - t₂| by linarith
 118    rw [← sub_le_iff_le_add]
 119    apply le_ciInf
 120    intro q
 121    have hle := ciInf_le (mcshane_bddBelow g_rat L hL t₁ h_g_lip) q
 122    have hm := mul_le_mul_of_nonneg_left (tri₂₁ q) hL
 123    linarith [show L * (|t₂ - (q : ℝ)| + |t₁ - t₂|) =
 124              L * |t₂ - (q : ℝ)| + L * |t₁ - t₂| from by ring]
 125
 126/-- **Lipschitz dense extension via McShane.**
 127
 128An L-Lipschitz function g_rat on ℚ extends to an L-Lipschitz g on ℝ.
 129Moreover, if f_n → g_rat at each rational and f_n is uniformly L-Lipschitz,
 130then f_n → g at every real t (the 3ε argument).
 131
 132The extension is the McShane upper extension: g(t) = inf_q (g_rat q + L|t-q|). -/
 133theorem lipschitz_dense_extension
 134    (f : ℕ → ℝ → ℝ) (L : ℝ) (hL : 0 ≤ L)
 135    (h_lip : ∀ n t₁ t₂, |f n t₁ - f n t₂| ≤ L * |t₁ - t₂|)
 136    (g_rat : ℚ → ℝ)
 137    (h_conv_rat : ∀ q : ℚ, Tendsto (fun n => f n (q : ℝ)) atTop (𝓝 (g_rat q)))
 138    (h_g_lip : ∀ q₁ q₂ : ℚ, |g_rat q₁ - g_rat q₂| ≤ L * |(q₁ : ℝ) - q₂|) :
 139    ∃ g : ℝ → ℝ,
 140      (∀ q : ℚ, g (q : ℝ) = g_rat q) ∧
 141      (∀ t₁ t₂, |g t₁ - g t₂| ≤ L * |t₁ - t₂|) ∧
 142      (∀ t : ℝ, Tendsto (fun n => f n t) atTop (𝓝 (g t))) := by
 143  let g : ℝ → ℝ := fun t => iInf (fun q : ℚ => g_rat q + L * |t - (q : ℝ)|)
 144  refine ⟨g, ?_, ?_, ?_⟩
 145  · intro q₀; exact mcshane_at_rat g_rat L hL q₀ h_g_lip
 146  · intro t₁ t₂; exact mcshane_lipschitz g_rat L hL h_g_lip t₁ t₂
 147  · -- 3ε argument: f_n → g at every real t
 148    intro t
 149    rw [Metric.tendsto_atTop]
 150    intro ε hε
 151    obtain ⟨q, hq⟩ := exists_rat_near t (show 0 < ε / (3 * (L + 1)) by positivity)
 152    have hgq : g (q : ℝ) = g_rat q := mcshane_at_rat g_rat L hL q h_g_lip
 153    have h_conv_q := h_conv_rat q
 154    rw [Metric.tendsto_atTop] at h_conv_q
 155    obtain ⟨N, hN⟩ := h_conv_q (ε / 3) (by positivity)
 156    refine ⟨N, fun n hn => ?_⟩
 157    rw [Real.dist_eq]
 158    have h1 : |f n t - f n (q : ℝ)| ≤ L * |t - (q : ℝ)| := h_lip n t q
 159    have h2 : |f n (q : ℝ) - g_rat q| < ε / 3 := by
 160      have := hN n hn; rwa [Real.dist_eq] at this
 161    have h3' : |g_rat q - g t| ≤ L * |t - (q : ℝ)| := by
 162      rw [← hgq]
 163      have hmc := mcshane_lipschitz g_rat L hL h_g_lip (q : ℝ) t
 164      rwa [abs_sub_comm (q : ℝ) t] at hmc
 165    have hLt : L * |t - (q : ℝ)| < ε / 3 := by
 166      have hpos : 0 < 3 * (L + 1) := by positivity
 167      calc L * |t - (q : ℝ)|
 168          ≤ (L + 1) * |t - (q : ℝ)| := by nlinarith [abs_nonneg (t - (q : ℝ))]
 169        _ < (L + 1) * (ε / (3 * (L + 1))) := by nlinarith [abs_nonneg (t - (q : ℝ))]
 170        _ = ε / 3 := by field_simp
 171    -- Triangle: |f n t - g t| ≤ |fn t - fn q| + |fn q - g_rat q| + |g_rat q - g t|
 172    have htri1 : |f n t - g t| ≤ |f n t - f n (q : ℝ)| + |f n (q : ℝ) - g t| := by
 173      have h := abs_add_le (f n t - f n (q : ℝ)) (f n (q : ℝ) - g t)
 174      have heq : (f n t - f n (q : ℝ)) + (f n (q : ℝ) - g t) = f n t - g t := by ring
 175      rwa [heq] at h
 176    have htri2 : |f n (q : ℝ) - g t| ≤ |f n (q : ℝ) - g_rat q| + |g_rat q - g t| := by
 177      have h := abs_add_le (f n (q : ℝ) - g_rat q) (g_rat q - g t)
 178      have heq : (f n (q : ℝ) - g_rat q) + (g_rat q - g t) = f n (q : ℝ) - g t := by ring
 179      rwa [heq] at h
 180    linarith
 181
 182end
 183
 184end IndisputableMonolith.NavierStokes.GalerkinEquicontinuity
 185