IndisputableMonolith.Gravity.Analysis.SpectralConvergence

   1import Mathlib
   2
   3/-!
   4# Spectral convergence toolkit: quantitative eigenvalue limits
   5
   6QG full-theory campaign, Phase 2a (reusable analysis toolkit).
   7
   8## Status: THEOREM (all results below are proved, axiom-clean; no sorry,
   9## no admit, no `: True` shells).
  10
  11## Lemmas and their campaign consumers
  12
  13* `eigenvalue_limit_of_uniform_bound`: a `C/N²` eventual bound on
  14  `|λ_N - Λ|` forces `λ_N → Λ`. Names the squeeze pattern that Phase 4
  15  (curved operator convergence) applies branch by branch.
  16* `sub_cube_le_sin` / `abs_sin_sub_le_cube`: the global cubic Taylor bound
  17  `|sin t - t| ≤ t³/6` for `t ≥ 0`, proved from
  18  `Real.one_sub_sq_div_two_le_cos` by a monotonicity argument. Mathlib's
  19  `Real.sin_bound` only covers `|t| ≤ 1`; this version has no smallness
  20  hypothesis, which the eigenvalue expansion below needs since `πk/N` is
  21  not small for large wavenumber `k`.
  22* `discrete_sine_eigenvalue_expansion`: the sharp quantitative version of
  23  the DiscreteLichnerowicz flat TT limit:
  24  `|4N² sin²(πk/N) - (2πk)²| ≤ ((2πk)⁴/12)/N²` for `N ≥ 1`. This upgrades
  25  the qualitative `Tendsto` of
  26  `IndisputableMonolith/Gravity/SevenGaps/DiscreteLichnerowicz.lean`
  27  (`discreteEigenvalue_tendsto`) to an explicit rate, which Phase 4 curved
  28  perturbation bounds consume.
  29* `discrete_sine_eigenvalue_tendsto`: the qualitative limit re-derived from
  30  the rate through `eigenvalue_limit_of_uniform_bound`, verifying that the
  31  two toolkit pieces compose.
  32* `spectrum_gap_persistence`: converging eigenvalue branches with distinct
  33  limits eventually separate. The tool Phase 4 uses to keep curved
  34  eigenvalue branches apart.
  35
  36## Downscope note
  37
  38The campaign brief listed a fourth target, `min_max_monotone_perturbation`
  39(Courant-Fischer transport of pointwise quadratic-form domination to
  40eigenvalue domination). Mathlib's `Matrix.IsHermitian` API (as vendored
  41here) provides eigenvalues via diagonalization but no min-max
  42characterization, so the transport is not cheap; it is recorded here as
  43future work rather than sunk time. Nothing below depends on it.
  44-/
  45
  46namespace IndisputableMonolith
  47namespace Gravity
  48namespace Analysis
  49
  50open Filter Topology
  51
  52/-- Helper: `C / N² → 0` as `N → ∞` over the naturals. -/
  53theorem const_div_sq_tendsto_zero (C : ℝ) :
  54    Filter.Tendsto (fun N : ℕ => C / (N : ℝ) ^ 2) Filter.atTop (nhds 0) := by
  55  have hpow : Filter.Tendsto (fun N : ℕ => ((N : ℝ)) ^ 2) Filter.atTop Filter.atTop := by
  56    have h1 : Filter.Tendsto (fun x : ℝ => x ^ 2) Filter.atTop Filter.atTop :=
  57      tendsto_pow_atTop two_ne_zero
  58    exact h1.comp tendsto_natCast_atTop_atTop
  59  exact tendsto_const_nhds.div_atTop hpow
  60
  61/-- THEOREM (squeeze with rate). If the discrete eigenvalues `lam N` satisfy
  62`|lam N - Λ| ≤ C/N²` for all `N ≥ N₀`, then `lam N → Λ`. Trivial, but it
  63names the pattern Phase 4 applies to every curved eigenvalue branch. -/
  64theorem eigenvalue_limit_of_uniform_bound (lam : ℕ → ℝ) (Λ C : ℝ) (N₀ : ℕ)
  65    (h : ∀ N : ℕ, N₀ ≤ N → |lam N - Λ| ≤ C / (N : ℝ) ^ 2) :
  66    Filter.Tendsto lam Filter.atTop (nhds Λ) := by
  67  rw [tendsto_iff_dist_tendsto_zero]
  68  refine squeeze_zero' (Filter.Eventually.of_forall fun N => dist_nonneg) ?_
  69    (const_div_sq_tendsto_zero C)
  70  filter_upwards [Filter.eventually_ge_atTop N₀] with N hN
  71  rw [Real.dist_eq]
  72  exact h N hN
  73
  74/-- THEOREM (global cubic sine lower bound). For `t ≥ 0`,
  75`t - t³/6 ≤ sin t`. Proof: `g(s) = sin s - s + s³/6` has derivative
  76`cos s - 1 + s²/2 ≥ 0` (by `Real.one_sub_sq_div_two_le_cos`), so `g` is
  77monotone and `g(t) ≥ g(0) = 0`. No smallness hypothesis on `t`. -/
  78theorem sub_cube_le_sin (t : ℝ) (ht : 0 ≤ t) :
  79    t - t ^ 3 / 6 ≤ Real.sin t := by
  80  have hderiv : ∀ s : ℝ,
  81      HasDerivAt (fun x : ℝ => Real.sin x - x + x ^ 3 / 6)
  82        (Real.cos s - 1 + (3 : ℝ) * s ^ 2 / 6) s := by
  83    intro s
  84    have hp : HasDerivAt (fun x : ℝ => x ^ 3) ((3 : ℝ) * s ^ 2) s := by
  85      have h := hasDerivAt_pow 3 s
  86      norm_num at h
  87      exact h
  88    exact ((Real.hasDerivAt_sin s).sub (hasDerivAt_id s)).add (hp.div_const 6)
  89  have hmono : Monotone (fun x : ℝ => Real.sin x - x + x ^ 3 / 6) := by
  90    refine monotone_of_hasDerivAt_nonneg hderiv ?_
  91    rw [Pi.le_def]
  92    intro s
  93    simp only [Pi.zero_apply]
  94    have hc := Real.one_sub_sq_div_two_le_cos (x := s)
  95    linarith
  96  have h0 : (fun x : ℝ => Real.sin x - x + x ^ 3 / 6) 0 = 0 := by
  97    simp
  98  have h := hmono ht
  99  rw [h0] at h
 100  simp only at h
 101  linarith
 102
 103/-- THEOREM (global cubic Taylor bound for sine). For `t ≥ 0`,
 104`|sin t - t| ≤ t³/6`. Combines `Real.sin_le` (upper) with
 105`sub_cube_le_sin` (lower). Unlike Mathlib's `Real.sin_bound`, no `|t| ≤ 1`
 106hypothesis is needed. -/
 107theorem abs_sin_sub_le_cube (t : ℝ) (ht : 0 ≤ t) :
 108    |Real.sin t - t| ≤ t ^ 3 / 6 := by
 109  have h1 : Real.sin t ≤ t := Real.sin_le ht
 110  have h2 : t - t ^ 3 / 6 ≤ Real.sin t := sub_cube_le_sin t ht
 111  have h3 : 0 ≤ t ^ 3 / 6 := by positivity
 112  rw [abs_le]
 113  constructor <;> linarith
 114
 115/-- THEOREM (quantitative flat TT eigenvalue expansion). For every
 116wavenumber `k` and lattice resolution `N ≥ 1`,
 117
 118`|4N² sin²(πk/N) - (2πk)²| ≤ ((2πk)⁴/12) / N²`.
 119
 120This is the sharp rate behind the qualitative limit
 121`DiscreteLichnerowicz.discreteEigenvalue_tendsto`. Derivation: with
 122`x = πk/N` we have `(2πk)² = 4N²x²`, so the error factors as
 123`4N² (sin x - x)(sin x + x)`; then `|sin x - x| ≤ x³/6`
 124(`abs_sin_sub_le_cube`) and `|sin x + x| ≤ 2x` give the bound
 125`(4/3) N² x⁴ = ((2πk)⁴/12)/N²`. Phase 4 curved perturbation bounds consume
 126this explicit constant `C(k) = (2πk)⁴/12`. -/
 127theorem discrete_sine_eigenvalue_expansion (k N : ℕ) (hN : 1 ≤ N) :
 128    |4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2
 129        - (2 * Real.pi * (k : ℝ)) ^ 2|
 130      ≤ (2 * Real.pi * (k : ℝ)) ^ 4 / 12 / (N : ℝ) ^ 2 := by
 131  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
 132  have hN0 : (N : ℝ) ≠ 0 := ne_of_gt hNpos
 133  set x : ℝ := Real.pi * (k : ℝ) / (N : ℝ) with hxdef
 134  have hx0 : 0 ≤ x := by
 135    rw [hxdef]
 136    exact div_nonneg (mul_nonneg Real.pi_pos.le (Nat.cast_nonneg k)) hNpos.le
 137  have hkey : (2 * Real.pi * (k : ℝ)) ^ 2 = 4 * (N : ℝ) ^ 2 * x ^ 2 := by
 138    rw [hxdef]
 139    field_simp
 140    ring
 141  have hfac : 4 * (N : ℝ) ^ 2 * Real.sin x ^ 2 - (2 * Real.pi * (k : ℝ)) ^ 2
 142      = (4 * (N : ℝ) ^ 2) * ((Real.sin x - x) * (Real.sin x + x)) := by
 143    rw [hkey]
 144    ring
 145  have h4N : |4 * (N : ℝ) ^ 2| = 4 * (N : ℝ) ^ 2 := abs_of_nonneg (by positivity)
 146  have hbound1 : |Real.sin x - x| ≤ x ^ 3 / 6 := abs_sin_sub_le_cube x hx0
 147  have hbound2 : |Real.sin x + x| ≤ 2 * x := by
 148    calc |Real.sin x + x| ≤ |Real.sin x| + |x| := abs_add_le _ _
 149      _ ≤ |x| + |x| := by
 150          have := Real.abs_sin_le_abs (x := x)
 151          linarith
 152      _ = 2 * x := by rw [abs_of_nonneg hx0]; ring
 153  calc |4 * (N : ℝ) ^ 2 * Real.sin x ^ 2 - (2 * Real.pi * (k : ℝ)) ^ 2|
 154      = (4 * (N : ℝ) ^ 2) * (|Real.sin x - x| * |Real.sin x + x|) := by
 155        rw [hfac, abs_mul, h4N, abs_mul]
 156    _ ≤ (4 * (N : ℝ) ^ 2) * (x ^ 3 / 6 * (2 * x)) := by
 157        refine mul_le_mul_of_nonneg_left ?_ (by positivity)
 158        exact mul_le_mul hbound1 hbound2 (abs_nonneg _) (by positivity)
 159    _ = (2 * Real.pi * (k : ℝ)) ^ 4 / 12 / (N : ℝ) ^ 2 := by
 160        rw [hxdef]
 161        field_simp
 162        ring
 163
 164/-- THEOREM (rated limit, composing the toolkit). The flat discrete TT
 165eigenvalue `4N² sin²(πk/N)` converges to `(2πk)²`, obtained by feeding the
 166quantitative expansion into `eigenvalue_limit_of_uniform_bound` with
 167`C = (2πk)⁴/12`. Re-derives
 168`DiscreteLichnerowicz.discreteEigenvalue_tendsto` with an explicit rate. -/
 169theorem discrete_sine_eigenvalue_tendsto (k : ℕ) :
 170    Filter.Tendsto
 171      (fun N : ℕ => 4 * (N : ℝ) ^ 2 * Real.sin (Real.pi * (k : ℝ) / (N : ℝ)) ^ 2)
 172      Filter.atTop (nhds ((2 * Real.pi * (k : ℝ)) ^ 2)) :=
 173  eigenvalue_limit_of_uniform_bound _ _ ((2 * Real.pi * (k : ℝ)) ^ 4 / 12) 1
 174    (fun N hN => discrete_sine_eigenvalue_expansion k N hN)
 175
 176/-- THEOREM (gap persistence). If two eigenvalue branches converge to
 177distinct limits `Λ < Μ`, then eventually `lam N < mu N`: spectral gaps
 178survive discretization for large `N`. The tool Phase 4 uses to separate
 179curved eigenvalue branches. -/
 180theorem spectrum_gap_persistence (lam mu : ℕ → ℝ) (Λ Μ : ℝ)
 181    (hlam : Filter.Tendsto lam Filter.atTop (nhds Λ))
 182    (hmu : Filter.Tendsto mu Filter.atTop (nhds Μ))
 183    (hlt : Λ < Μ) :
 184    ∀ᶠ N : ℕ in Filter.atTop, lam N < mu N :=
 185  hlam.eventually_lt hmu hlt
 186
 187end Analysis
 188end Gravity
 189end IndisputableMonolith
 190