IndisputableMonolith.ClassicalBridge.Fluids.ContinuumLimit2D

   1import Mathlib
   2import IndisputableMonolith.ClassicalBridge.Fluids.Galerkin2D
   3import IndisputableMonolith.ClassicalBridge.Fluids.CPM2D
   4
   5namespace IndisputableMonolith.ClassicalBridge.Fluids
   6
   7open Real
   8open Filter
   9open Topology
  10open scoped InnerProductSpace
  11
  12/-!
  13# ContinuumLimit2D (Milestone M5)
  14
  15This file defines a *Lean-checkable pipeline shape* for passing from a family of finite-dimensional
  162D Galerkin approximations to a “continuum” limit object.
  17
  18At this milestone we stay honest about what is and is not formalized:
  19- we define the relevant objects (an infinite Fourier coefficient state),
  20- we define the canonical embedding of truncated coefficients into the full Fourier state, and
  21- we package the analytic compactness/identification steps as explicit hypotheses (no `axiom`, no `sorry`).
  22
  23The point is to make the dependency graph explicit so that later milestones can progressively
  24replace hypotheses with proofs.
  25-/
  26
  27namespace ContinuumLimit2D
  28
  29/-!
  30## Continuum Fourier state on 𝕋²
  31
  32We model a 2D torus velocity field via its Fourier coefficients:
  33for each `k : Mode2 = ℤ×ℤ`, a coefficient `VelCoeff = EuclideanSpace ℝ (Fin 2)`.
  34-/
  35
  36/-- Full (infinite) Fourier coefficient state for a 2D velocity field on 𝕋². -/
  37abbrev FourierState2D : Type := Mode2 → VelCoeff
  38
  39/-!
  40## Embedding: GalerkinState N → FourierState2D
  41
  42We extend a truncated state by zero outside the truncation window.
  43-/
  44
  45/-- Read a single component coefficient at mode `k` (zero if `k ∉ modes N`). -/
  46noncomputable def coeffAt {N : ℕ} (u : GalerkinState N) (k : Mode2) (j : Fin 2) : ℝ :=
  47  if hk : k ∈ modes N then
  48    -- `k` as an element of the finite index type `(modes N)`
  49    let k' : (modes N) := ⟨k, hk⟩
  50    u (k', j)
  51  else
  52    0
  53
  54/-- Extend a truncated Galerkin state by zero to a full Fourier coefficient state. -/
  55noncomputable def extendByZero {N : ℕ} (u : GalerkinState N) : FourierState2D :=
  56  fun k =>
  57    -- Build a 2-vector coefficient from its two components.
  58    !₂[coeffAt u k ⟨0, by decide⟩, coeffAt u k ⟨1, by decide⟩]
  59
  60/-!
  61## Linearity of the zero-extension embedding
  62
  63We will eventually want to pass (linear) identities from Galerkin trajectories to limits.
  64For that, it is useful to record that `extendByZero` is a linear map.
  65-/
  66
  67lemma coeffAt_add {N : ℕ} (u v : GalerkinState N) (k : Mode2) (j : Fin 2) :
  68    coeffAt (u + v) k j = coeffAt u k j + coeffAt v k j := by
  69  classical
  70  by_cases hk : k ∈ modes N
  71  · simp [coeffAt, hk]
  72  · simp [coeffAt, hk]
  73
  74lemma coeffAt_smul {N : ℕ} (c : ℝ) (u : GalerkinState N) (k : Mode2) (j : Fin 2) :
  75    coeffAt (c • u) k j = c * coeffAt u k j := by
  76  classical
  77  by_cases hk : k ∈ modes N
  78  · simp [coeffAt, hk]
  79  · simp [coeffAt, hk]
  80
  81lemma extendByZero_add {N : ℕ} (u v : GalerkinState N) :
  82    extendByZero (u + v) = extendByZero u + extendByZero v := by
  83  classical
  84  funext k
  85  ext j
  86  fin_cases j <;> simp [extendByZero, coeffAt_add]
  87
  88lemma extendByZero_smul {N : ℕ} (c : ℝ) (u : GalerkinState N) :
  89    extendByZero (c • u) = c • (extendByZero u) := by
  90  classical
  91  funext k
  92  ext j
  93  fin_cases j <;> simp [extendByZero, coeffAt_smul]
  94
  95lemma extendByZero_neg {N : ℕ} (u : GalerkinState N) :
  96    extendByZero (-u) = -extendByZero u := by
  97  classical
  98  -- `-u = (-1) • u` and `extendByZero` is linear.
  99  simpa [neg_one_smul] using (extendByZero_smul (N := N) (-1) u)
 100
 101/-- `extendByZero` packaged as a linear map. -/
 102noncomputable def extendByZeroLinear (N : ℕ) : GalerkinState N →ₗ[ℝ] FourierState2D :=
 103  { toFun := extendByZero
 104    map_add' := extendByZero_add (N := N)
 105    map_smul' := by
 106      intro c u
 107      -- `simp` expects `c • x`; our lemma is stated in that form.
 108      simpa using (extendByZero_smul (N := N) c u) }
 109
 110/-- `extendByZero` as a *continuous* linear map.
 111
 112This is available because `GalerkinState N` is finite-dimensional, hence every linear map out of it
 113is continuous. -/
 114noncomputable def extendByZeroCLM (N : ℕ) : GalerkinState N →L[ℝ] FourierState2D :=
 115  LinearMap.toContinuousLinearMap (extendByZeroLinear N)
 116
 117/-!
 118## Divergence-free structure (Fourier side) and limit stability
 119
 120A structural property we can pass to the limit using only modewise convergence is a closed,
 121linear constraint such as “divergence-free in Fourier variables”:
 122
 123`k₁ * û₁(t,k) + k₂ * û₂(t,k) = 0` for every mode `k`.
 124-/
 125
 126/-- Real Fourier-side divergence constraint for a single mode. -/
 127noncomputable def divConstraint (k : Mode2) (v : VelCoeff) : ℝ :=
 128  (k.1 : ℝ) * v (0 : Fin 2) + (k.2 : ℝ) * v (1 : Fin 2)
 129
 130/-- Fourier-side divergence-free predicate (modewise, at a fixed time). -/
 131def IsDivergenceFree (u : FourierState2D) : Prop :=
 132  ∀ k : Mode2, divConstraint k (u k) = 0
 133
 134/-- Divergence-free predicate for a time-dependent Fourier trajectory. -/
 135def IsDivergenceFreeTraj (u : ℝ → FourierState2D) : Prop :=
 136  ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((u t) k) = 0
 137
 138lemma divConstraint_continuous (k : Mode2) : Continuous fun v : VelCoeff => divConstraint k v := by
 139  have h0 : Continuous fun v : VelCoeff => v (0 : Fin 2) := by
 140    simpa using
 141      (PiLp.continuous_apply (p := (2 : ENNReal)) (β := fun _ : Fin 2 => ℝ) (0 : Fin 2))
 142  have h1 : Continuous fun v : VelCoeff => v (1 : Fin 2) := by
 143    simpa using
 144      (PiLp.continuous_apply (p := (2 : ENNReal)) (β := fun _ : Fin 2 => ℝ) (1 : Fin 2))
 145  simpa [divConstraint] using ((continuous_const.mul h0).add (continuous_const.mul h1))
 146
 147/-!
 148## Linear Stokes/heat mild form (Fourier side) and limit stability
 149
 150As a next step toward a real PDE statement, we can talk about the *linear* (viscous) dynamics.
 151On the Fourier side, the Stokes/heat semigroup acts diagonally:
 152
 153`û(t,k) = exp(-ν |k|^2 t) • û(0,k)`.
 154
 155This is still not Navier–Stokes, but it is a concrete PDE-like identity that can be passed to the
 156limit using only modewise convergence (no compactness beyond that).
 157-/
 158
 159/-- Fourier-side heat/Stokes factor `e^{-ν|k|^2 t}`. -/
 160noncomputable def heatFactor (ν : ℝ) (t : ℝ) (k : Mode2) : ℝ :=
 161  Real.exp (-ν * kSq k * t)
 162
 163/-- Mild Stokes/heat solution in Fourier coefficients (modewise, for `t ≥ 0`). -/
 164def IsStokesMildTraj (ν : ℝ) (u : ℝ → FourierState2D) : Prop :=
 165  ∀ t ≥ 0, ∀ k : Mode2, (u t) k = (heatFactor ν t k) • (u 0) k
 166
 167/-- Differential (within `t ≥ 0`) Stokes/heat equation in Fourier coefficients (modewise).
 168
 169This is a slightly more “PDE-like” statement than the mild form: for each fixed mode `k`,
 170the coefficient trajectory satisfies
 171
 172`d/dt u(t,k) = -(ν |k|^2) • u(t,k)`
 173
 174as a derivative **within** the half-line `[0,∞)`. -/
 175def IsStokesODETraj (ν : ℝ) (u : ℝ → FourierState2D) : Prop :=
 176  ∀ t ≥ 0, ∀ k : Mode2,
 177    HasDerivWithinAt (fun s : ℝ => (u s) k) (-(ν * kSq k) • (u t) k) (Set.Ici (0 : ℝ)) t
 178
 179/-!
 180## First nonlinear (Duhamel-style) identification: heat evolution + remainder
 181
 182To start introducing the nonlinear Navier–Stokes term without committing to the full analytic
 183infrastructure (time integrals, dominated convergence, etc.), we use a *Duhamel-like remainder*
 184term `D(t,k)`:
 185
 186`u(t,k) = heatFactor(ν,t,k) • u(0,k) + D(t,k)`.
 187
 188In a future milestone, `D` will be instantiated as the time-integrated nonlinear forcing.
 189For now, this already gives a useful “nonlinear-shaped” identity that can be passed to the limit
 190under modewise convergence, provided the remainders also converge modewise.
 191-/
 192
 193/-- Duhamel-style (nonlinear) remainder form: `u = heatFactor • u0 + D` (modewise, for `t ≥ 0`). -/
 194def IsNSDuhamelTraj (ν : ℝ) (D : ℝ → FourierState2D) (u : ℝ → FourierState2D) : Prop :=
 195  ∀ t ≥ 0, ∀ k : Mode2, (u t) k = (heatFactor ν t k) • (u 0) k + (D t) k
 196
 197namespace IsStokesMildTraj
 198
 199/-- Mild Stokes/heat identity implies the corresponding differential equation (within `t ≥ 0`). -/
 200theorem stokesODE {ν : ℝ} {u : ℝ → FourierState2D} (h : IsStokesMildTraj ν u) :
 201    IsStokesODETraj ν u := by
 202  intro t ht k
 203  -- Let `a = u(0,k)` so the mild formula reads `u(s,k) = exp(-ν|k|^2 s) • a` for `s ≥ 0`.
 204  let a : VelCoeff := (u 0) k
 205
 206  -- Derivative of the scalar heat factor.
 207  have hlin : HasDerivAt (fun s : ℝ => (-ν * kSq k) * s) (-ν * kSq k) t := by
 208    simpa [mul_assoc] using (hasDerivAt_id t).const_mul (-ν * kSq k)
 209  have hscalar :
 210      HasDerivAt (fun s : ℝ => heatFactor ν s k)
 211        (heatFactor ν t k * (-ν * kSq k)) t := by
 212    -- `d/ds exp(g(s)) = exp(g(s)) * g'(s)` with `g(s) = (-ν|k|^2) * s`.
 213    have hexp :
 214        HasDerivAt (fun s : ℝ => Real.exp ((-ν * kSq k) * s))
 215          (Real.exp ((-ν * kSq k) * t) * (-ν * kSq k)) t :=
 216      (Real.hasDerivAt_exp ((-ν * kSq k) * t)).comp t hlin
 217    simpa [heatFactor, mul_assoc] using hexp
 218  have hscalarW :
 219      HasDerivWithinAt (fun s : ℝ => heatFactor ν s k)
 220        (heatFactor ν t k * (-ν * kSq k)) (Set.Ici (0 : ℝ)) t :=
 221    hscalar.hasDerivWithinAt
 222
 223  -- Differentiate `s ↦ heatFactor ν s k • a` within `[0,∞)`.
 224  have hform :
 225      HasDerivWithinAt (fun s : ℝ => (heatFactor ν s k) • a)
 226        ((heatFactor ν t k * (-ν * kSq k)) • a) (Set.Ici (0 : ℝ)) t :=
 227    hscalarW.smul_const a
 228
 229  -- Replace the formula by `u` using the mild identity on the domain `[0,∞)`.
 230  have huEq : ∀ s ∈ Set.Ici (0 : ℝ), (fun s : ℝ => (u s) k) s = (fun s : ℝ => (heatFactor ν s k) • a) s := by
 231    intro s hs
 232    -- `hs : 0 ≤ s`
 233    simpa [a] using (h s hs k)
 234  have huEq_t : (fun s : ℝ => (u s) k) t = (fun s : ℝ => (heatFactor ν s k) • a) t := by
 235    simpa [a] using (h t ht k)
 236
 237  have huDeriv :
 238      HasDerivWithinAt (fun s : ℝ => (u s) k) ((heatFactor ν t k * (-ν * kSq k)) • a)
 239        (Set.Ici (0 : ℝ)) t :=
 240    hform.congr huEq huEq_t
 241
 242  -- Simplify the derivative into `-(ν|k|^2) • u(t,k)`.
 243  have hsimp :
 244      ((heatFactor ν t k * (-ν * kSq k)) • a) = (-(ν * kSq k)) • ((u t) k) := by
 245    -- Use commutativity of real multiplication to flip the order, then `mul_smul`.
 246    have hut : (u t) k = (heatFactor ν t k) • a := by
 247      simpa [a] using (h t ht k)
 248    -- Rewrite to match `mul_smul` and then substitute `hut`.
 249    calc
 250      (heatFactor ν t k * (-ν * kSq k)) • a
 251          = ((-ν * kSq k) * heatFactor ν t k) • a := by
 252              simp [mul_comm, mul_assoc]
 253      _ = (-ν * kSq k) • ((heatFactor ν t k) • a) := by
 254              simp [mul_smul]
 255      _ = (-(ν * kSq k)) • ((heatFactor ν t k) • a) := by ring_nf
 256      _ = (-(ν * kSq k)) • ((u t) k) := by simp [hut]
 257
 258  -- `simp` may rewrite `heatFactor * (-ν*kSq)` as `-(heatFactor * (ν*kSq))`, so we also register
 259  -- a simp-friendly variant with the outer negation.
 260  have hsimp_neg :
 261      -((heatFactor ν t k * (ν * kSq k)) • a) = (-(ν * kSq k)) • ((u t) k) := by
 262    -- Move the `-` inside as `(-1) • _` and simplify using `hsimp`.
 263    have : (heatFactor ν t k * (-ν * kSq k)) • a = -((heatFactor ν t k * (ν * kSq k)) • a) := by
 264      -- scalar arithmetic in `ℝ` + `(-r) • a = -(r • a)`
 265      calc
 266        (heatFactor ν t k * (-ν * kSq k)) • a
 267            = (-(heatFactor ν t k * (ν * kSq k))) • a := by ring_nf
 268        _ = -((heatFactor ν t k * (ν * kSq k)) • a) := by
 269            simp [neg_smul]
 270    -- Now rewrite and finish.
 271    simpa [this] using hsimp
 272
 273  simpa [IsStokesODETraj, hsimp_neg] using huDeriv
 274
 275end IsStokesMildTraj
 276
 277/-!
 278## Galerkin → Fourier coefficient dynamics (modewise ODE, with nonlinearity)
 279
 280This is the first genuinely “Navier–Stokes shaped” bridge lemma: if a Galerkin trajectory satisfies
 281the finite-dimensional ODE `u' = νΔu - B(u,u)`, then every Fourier mode of its zero-extension
 282satisfies the corresponding modewise ODE with a forcing given by the zero-extended nonlinear term.
 283-/
 284
 285lemma extendByZero_laplacianCoeff {N : ℕ} (u : GalerkinState N) (k : Mode2) :
 286    (extendByZero (laplacianCoeff (N := N) u)) k = (-kSq k) • (extendByZero u) k := by
 287  classical
 288  by_cases hk : k ∈ modes N
 289  · ext j
 290    fin_cases j <;> simp [extendByZero, coeffAt, hk, laplacianCoeff]
 291  · ext j
 292    fin_cases j <;> simp [extendByZero, coeffAt, hk]
 293
 294lemma hasDerivAt_extendByZero_apply {N : ℕ} (k : Mode2)
 295    (u : ℝ → GalerkinState N) (u' : GalerkinState N) {t : ℝ} (hu : HasDerivAt u u' t) :
 296    HasDerivAt (fun s : ℝ => (extendByZero (u s)) k) ((extendByZero u') k) t := by
 297  classical
 298  -- A constant continuous linear map: project the `k`-th Fourier coefficient after zero-extension.
 299  let L : GalerkinState N →L[ℝ] VelCoeff :=
 300    (ContinuousLinearMap.proj k).comp (extendByZeroCLM (N := N))
 301  have hL : HasDerivAt (fun _ : ℝ => L) 0 t := by
 302    simpa using (hasDerivAt_const (x := t) (c := L))
 303  -- Differentiate `s ↦ L (u s)`.
 304  have h := HasDerivAt.clm_apply (c := fun _ : ℝ => L) (c' := (0 : GalerkinState N →L[ℝ] VelCoeff))
 305    (u := u) (u' := u') (x := t) hL hu
 306  -- Unfold `L` back to `extendByZero` + evaluation at `k`.
 307  simpa [L, extendByZeroCLM] using h
 308
 309theorem galerkinNS_hasDerivAt_extendByZero_mode {N : ℕ} (ν : ℝ) (B : ConvectionOp N)
 310    (u : ℝ → GalerkinState N) (k : Mode2) {t : ℝ}
 311    (hu : HasDerivAt u (galerkinNSRHS (N := N) ν B (u t)) t) :
 312    HasDerivAt (fun s : ℝ => (extendByZero (u s)) k)
 313      ((ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k) t := by
 314  -- Start from the generic differentiation-through-zero-extension lemma.
 315  have h0 :
 316      HasDerivAt (fun s : ℝ => (extendByZero (u s)) k)
 317        ((extendByZero (galerkinNSRHS (N := N) ν B (u t))) k) t :=
 318    hasDerivAt_extendByZero_apply (N := N) k u (galerkinNSRHS (N := N) ν B (u t)) hu
 319  -- Simplify the RHS using linearity of `extendByZero` and the diagonal Laplacian.
 320  -- `extendByZero (ν•Δu - B(u,u)) = ν•extendByZero(Δu) - extendByZero(B(u,u))`
 321  have hR :
 322      (extendByZero (galerkinNSRHS (N := N) ν B (u t)) k)
 323        = (ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k := by
 324    -- Push `extendByZero` through the RHS definition.
 325    simp [galerkinNSRHS, extendByZero_smul, extendByZero_add, extendByZero_neg,
 326      extendByZero_laplacianCoeff, sub_eq_add_neg, mul_smul]
 327  -- Rewrite the derivative statement with the simplified RHS.
 328  simpa [hR] using h0
 329
 330/-!
 331## Connecting the nonlinear forcing to the Duhamel remainder (modewise, differential form)
 332
 333We define a *Duhamel remainder* for a Galerkin trajectory by subtracting the linear heat evolution
 334of the initial coefficient. Then the modewise Galerkin ODE implies a forced linear ODE for this
 335remainder with forcing given by the zero-extended nonlinear term.
 336
 337This is not yet the full integral (variation-of-constants) formula, but it ties the remainder to
 338the Galerkin nonlinearity in a way that can later be integrated.
 339-/
 340
 341/-- Duhamel remainder (Galerkin → Fourier, modewise):
 342
 343`R(t,k) := û(t,k) - heatFactor(ν,t,k) • û(0,k)`. -/
 344noncomputable def duhamelRemainderOfGalerkin {N : ℕ} (ν : ℝ) (u : ℝ → GalerkinState N) : ℝ → FourierState2D :=
 345  fun t k => (extendByZero (u t) k) - (heatFactor ν t k) • (extendByZero (u 0) k)
 346
 347/-- If a Galerkin trajectory satisfies the discrete NS ODE, then its Duhamel remainder satisfies a
 348forced linear ODE per mode, with forcing `-(extendByZero (B(u,u)))`.
 349
 350This is the differential version of the Duhamel/variation-of-constants formula. -/
 351theorem galerkinNS_hasDerivAt_duhamelRemainder_mode {N : ℕ} (ν : ℝ) (B : ConvectionOp N)
 352    (u : ℝ → GalerkinState N) (k : Mode2) {t : ℝ}
 353    (hu : HasDerivAt u (galerkinNSRHS (N := N) ν B (u t)) t) :
 354    HasDerivAt (fun s : ℝ => (duhamelRemainderOfGalerkin (N := N) ν u s) k)
 355      ((ν * (-kSq k)) • (duhamelRemainderOfGalerkin (N := N) ν u t k) - (extendByZero (B (u t) (u t))) k) t := by
 356  classical
 357  -- shorthand
 358  let a0 : VelCoeff := (extendByZero (u 0)) k
 359
 360  -- derivative of the main coefficient from the Galerkin ODE
 361  have ha :
 362      HasDerivAt (fun s : ℝ => (extendByZero (u s)) k)
 363        ((ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k) t :=
 364    galerkinNS_hasDerivAt_extendByZero_mode (N := N) (ν := ν) (B := B) (u := u) (k := k) hu
 365
 366  -- derivative of the linear heat term `s ↦ heatFactor ν s k • a0`
 367  have hlin : HasDerivAt (fun s : ℝ => (-ν * kSq k) * s) (-ν * kSq k) t := by
 368    simpa [mul_assoc] using (hasDerivAt_id t).const_mul (-ν * kSq k)
 369  have hscalar :
 370      HasDerivAt (fun s : ℝ => heatFactor ν s k) (heatFactor ν t k * (-ν * kSq k)) t := by
 371    have hexp :
 372        HasDerivAt (fun s : ℝ => Real.exp ((-ν * kSq k) * s))
 373          (Real.exp ((-ν * kSq k) * t) * (-ν * kSq k)) t :=
 374      (Real.hasDerivAt_exp ((-ν * kSq k) * t)).comp t hlin
 375    simpa [heatFactor, mul_assoc] using hexp
 376  have hb :
 377      HasDerivAt (fun s : ℝ => (heatFactor ν s k) • a0)
 378        ((heatFactor ν t k * (-ν * kSq k)) • a0) t :=
 379    hscalar.smul_const a0
 380
 381  -- differentiate the difference
 382  have hsub :
 383      HasDerivAt (fun s : ℝ => (extendByZero (u s)) k - (heatFactor ν s k) • a0)
 384        (((ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k)
 385          - ((heatFactor ν t k * (-ν * kSq k)) • a0)) t := by
 386    -- Do not `simpa` here: we want to keep the derivative expression in a form that
 387    -- matches the subsequent algebraic rewrite.
 388    simpa [sub_eq_add_neg] using ha.sub hb
 389
 390  -- rewrite the derivative into the forced-remainder form
 391  have hb' :
 392      (heatFactor ν t k * (-ν * kSq k)) • a0 = (ν * (-kSq k)) • ((heatFactor ν t k) • a0) := by
 393    calc
 394      (heatFactor ν t k * (-ν * kSq k)) • a0
 395          = ((-ν * kSq k) * heatFactor ν t k) • a0 := by
 396              simp [mul_comm, mul_assoc]
 397      _ = (-ν * kSq k) • ((heatFactor ν t k) • a0) := by
 398              simp [mul_smul]
 399      _ = (ν * (-kSq k)) • ((heatFactor ν t k) • a0) := by ring_nf
 400
 401  have hderiv_simp :
 402      (((ν * (-kSq k)) • (extendByZero (u t)) k - (extendByZero (B (u t) (u t))) k)
 403          - ((heatFactor ν t k * (-ν * kSq k)) • a0))
 404        = ((ν * (-kSq k)) • ((extendByZero (u t)) k - (heatFactor ν t k) • a0)
 405            - (extendByZero (B (u t) (u t))) k) := by
 406    -- push the scalar through the subtraction and use the rewritten `hb'`
 407    -- First rewrite the heat-term derivative using `hb'`, then reduce to commutative-additive algebra.
 408    rw [hb']
 409    -- Expand `c • (x - y)` and rewrite subtraction as addition; then commutativity closes the goal.
 410    simp [sub_eq_add_neg, add_left_comm, add_comm]
 411
 412  -- conclude
 413  have hsub' :
 414      HasDerivAt (fun s : ℝ => (extendByZero (u s)) k - (heatFactor ν s k) • a0)
 415        ((ν * (-kSq k)) • ((extendByZero (u t)) k - (heatFactor ν t k) • a0)
 416          - (extendByZero (B (u t) (u t))) k) t := by
 417    -- Avoid `simp` rewriting the derivative expression (it tends to normalize `ν * (-kSq)` into `-(ν*kSq)`).
 418    -- Instead, rewrite the goal using the proved algebraic identity `hderiv_simp`.
 419    rw [← hderiv_simp]
 420    exact hsub
 421
 422  simpa [duhamelRemainderOfGalerkin, a0] using hsub'
 423
 424/-- Variation-of-constants / Duhamel (integrating factor) formula for the Galerkin remainder (modewise).
 425
 426This upgrades the forced remainder ODE to an **integral** identity, assuming the forcing term is
 427interval-integrable.
 428
 429Note: This is an integrating-factor form; rewriting it into the usual kernel `heatFactor ν (t-s) k`
 430is a later algebraic step (plus a change-of-variables in the integral). -/
 431theorem duhamelRemainderOfGalerkin_integratingFactor
 432    {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) (t : ℝ)
 433    (hu : ∀ s : ℝ, HasDerivAt u (galerkinNSRHS (N := N) ν B (u s)) s)
 434    (hint :
 435      IntervalIntegrable (fun s : ℝ =>
 436        (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 437        MeasureTheory.volume 0 t) :
 438    (Real.exp (-(ν * (-kSq k)) * t)) • (duhamelRemainderOfGalerkin (N := N) ν u t k)
 439      =
 440        -∫ s in (0 : ℝ)..t, (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k) := by
 441  classical
 442  -- Notation
 443  let a : ℝ := ν * (-kSq k)
 444  let E : ℝ → ℝ := fun s => Real.exp (-a * s)
 445  let R : ℝ → VelCoeff := fun s => (duhamelRemainderOfGalerkin (N := N) ν u s) k
 446  let F : ℝ → VelCoeff := fun s => (extendByZero (B (u s) (u s))) k
 447  let G : ℝ → VelCoeff := fun s => (E s) • (R s)
 448
 449  have hE : ∀ x : ℝ, HasDerivAt E (-(E x * a)) x := by
 450    intro x
 451    have hlin : HasDerivAt (fun s : ℝ => (-a) * s) (-a) x := by
 452      simpa [mul_assoc] using (hasDerivAt_id x).const_mul (-a)
 453    have hexp :
 454        HasDerivAt (fun s : ℝ => Real.exp ((-a) * s)) (Real.exp ((-a) * x) * (-a)) x :=
 455      (Real.hasDerivAt_exp ((-a) * x)).comp x hlin
 456    -- rewrite `r * (-a)` as `-(r * a)`
 457    simpa [E, mul_assoc, mul_neg] using hexp
 458
 459  have hR : ∀ x : ℝ, HasDerivAt R (a • R x - F x) x := by
 460    intro x
 461    -- Remainder ODE at time `x`
 462    simpa [R, F, a] using
 463      (galerkinNS_hasDerivAt_duhamelRemainder_mode (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := x)
 464        (hu x))
 465
 466  have hGderiv : ∀ x ∈ Set.uIcc (0 : ℝ) t, HasDerivAt G (-((E x) • (F x))) x := by
 467    intro x _hx
 468    have hG0 : HasDerivAt G ((E x) • (a • R x - F x) + (-(E x * a)) • R x) x :=
 469      (hE x).smul (hR x)
 470    have hG0' : HasDerivAt G ((E x) • (a • R x - F x) + -((E x * a) • R x)) x := by
 471      simpa [neg_smul] using hG0
 472    -- Simplify: the `a • R` terms cancel, leaving `-(E x • F x)`.
 473    have hsimp :
 474        (E x) • (a • R x - F x) + -((E x * a) • R x) = -((E x) • (F x)) := by
 475      -- Expand `E • (a • R - F)` and cancel the `a • R` terms.
 476      calc
 477        (E x) • (a • R x - F x) + -((E x * a) • R x)
 478            = (E x) • (a • R x - F x) - (E x * a) • R x := by
 479                simp [sub_eq_add_neg]
 480        _ = (E x) • (a • R x) - (E x) • (F x) - (E x * a) • R x := by
 481                simp [sub_eq_add_neg, add_assoc]
 482        _ = (E x * a) • R x - (E x) • (F x) - (E x * a) • R x := by
 483                simp [smul_smul]
 484        _ = -((E x) • (F x)) := by abel
 485    simpa [G, hsimp] using hG0'
 486
 487  -- Integrate the derivative of `G` on `0..t`.
 488  have hint' : IntervalIntegrable (fun s : ℝ => -((E s) • (F s))) MeasureTheory.volume 0 t := by
 489    -- our hypothesis is stated for `Real.exp (-(ν * (-kSq k)) * s)`, which is `E s` by definition
 490    -- and `F s` is the nonlinear term.
 491    -- `IntervalIntegrable.neg` handles the outer `-`.
 492    have : IntervalIntegrable (fun s : ℝ => (E s) • (F s)) MeasureTheory.volume 0 t := by
 493      simpa [E, F, a] using hint
 494    simpa using this.neg
 495
 496  have hFTC :
 497      (∫ s in (0 : ℝ)..t, -((E s) • (F s))) = G t - G 0 :=
 498    intervalIntegral.integral_eq_sub_of_hasDerivAt (a := (0 : ℝ)) (b := t)
 499      (hderiv := hGderiv) (hint := hint')
 500
 501  have hR0 : R 0 = 0 := by
 502    -- `R 0 = û(0,k) - heatFactor(0)•û(0,k) = 0`
 503    simp [R, duhamelRemainderOfGalerkin, heatFactor]
 504
 505  have hG0 : G 0 = 0 := by
 506    simp [G, E, hR0]
 507
 508  -- Rewrite the result in the desired form.
 509  have hEq : (E t) • (R t) = ∫ s in (0 : ℝ)..t, -((E s) • (F s)) := by
 510    -- `hFTC` gives the integral equals `G t - G 0`; and `G 0 = 0`.
 511    have : (∫ s in (0 : ℝ)..t, -((E s) • (F s))) = (E t) • (R t) := by
 512      simpa [hG0, G] using hFTC
 513    exact this.symm
 514
 515  have hEq' : (E t) • (R t) = -∫ s in (0 : ℝ)..t, (E s) • (F s) := by
 516    calc
 517      (E t) • (R t) = ∫ s in (0 : ℝ)..t, -((E s) • (F s)) := hEq
 518      _ = -∫ s in (0 : ℝ)..t, (E s) • (F s) := by simp
 519
 520  simpa [E, R, F, a] using hEq'
 521
 522/-- Rewrite the integrating-factor remainder formula into the standard Duhamel kernel form:
 523
 524`R(t,k) = -∫₀ᵗ heatFactor ν (t - s) k • F(s,k) ds`.
 525
 526This is a purely algebraic rewrite of `duhamelRemainderOfGalerkin_integratingFactor`. -/
 527theorem duhamelRemainderOfGalerkin_kernel
 528    {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) (t : ℝ)
 529    (hu : ∀ s : ℝ, HasDerivAt u (galerkinNSRHS (N := N) ν B (u s)) s)
 530    (hint :
 531      IntervalIntegrable (fun s : ℝ =>
 532        (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 533        MeasureTheory.volume 0 t) :
 534    duhamelRemainderOfGalerkin (N := N) ν u t k
 535      =
 536        -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
 537  -- Start from the integrating-factor identity.
 538  have hIF :=
 539    duhamelRemainderOfGalerkin_integratingFactor (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := t) hu hint
 540
 541  -- Multiply both sides by the heat factor at time `t` to cancel the integrating factor.
 542  have hmul : (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 543      =
 544        (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
 545          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)) := by
 546    simpa using congrArg (fun v => (heatFactor ν t k) • v) hIF
 547
 548  -- Simplify the left-hand side: `heatFactor(t) * exp(ν|k|^2 t) = 1`.
 549  have hcancel :
 550      (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 551        = duhamelRemainderOfGalerkin (N := N) ν u t k := by
 552    -- turn nested smul into product scalar
 553    have hprod : (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t)) = 1 := by
 554      calc
 555        (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t))
 556            = Real.exp (-ν * kSq k * t) * Real.exp (ν * kSq k * t) := by
 557                simp [heatFactor]
 558        _ = Real.exp ((-ν * kSq k * t) + (ν * kSq k * t)) := (Real.exp_add _ _).symm
 559        _ = Real.exp 0 := by ring_nf
 560        _ = 1 := by simp
 561    calc
 562      (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k)
 563          = ((heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * t))) • duhamelRemainderOfGalerkin (N := N) ν u t k := by
 564              simp [smul_smul]
 565      _ = (1 : ℝ) • duhamelRemainderOfGalerkin (N := N) ν u t k := by
 566            -- avoid `simp` rewriting the exponential before applying `hprod`
 567            rw [hprod]
 568      _ = duhamelRemainderOfGalerkin (N := N) ν u t k := by simp
 569
 570  -- Move the scalar inside the integral, then combine the exponentials into `heatFactor ν (t - s) k`.
 571  have hRHS :
 572      (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
 573          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 574        =
 575        -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
 576    -- Let `f(s)` be the integrand in the integrating-factor identity.
 577    let f : ℝ → VelCoeff :=
 578      fun s => (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)
 579    -- First move the scalar inside the integral.
 580    have hsmul :
 581        (heatFactor ν t k) • (∫ s in (0 : ℝ)..t, f s) =
 582          ∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := by
 583      simp [f]
 584    -- Rewrite `heatFactor ν t k • (-∫ f)` as `-∫ (heatFactor ν t k • f)`.
 585    have hneg :
 586        (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t, f s)
 587          = -∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := by
 588      calc
 589        (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t, f s)
 590            = -((heatFactor ν t k) • (∫ s in (0 : ℝ)..t, f s)) := by simp [smul_neg]
 591        _ = -(∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s)) := by rw [hsmul]
 592        _ = -∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := rfl
 593    -- Now simplify the integrand pointwise on the integration interval.
 594    have hEqOn :
 595        Set.EqOn (fun s => (heatFactor ν t k) • (f s))
 596          (fun s => (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k)) (Set.uIcc (0 : ℝ) t) := by
 597      intro s _hs
 598      -- combine scalar factors into `heatFactor ν (t - s) k`
 599      have hscalar :
 600          (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * s)) = heatFactor ν (t - s) k := by
 601        calc
 602          (heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * s))
 603              = Real.exp (-ν * kSq k * t) * Real.exp (ν * kSq k * s) := by
 604                  simp [heatFactor]
 605          _ = Real.exp ((-ν * kSq k * t) + (ν * kSq k * s)) := (Real.exp_add _ _).symm
 606          _ = Real.exp (-ν * kSq k * (t - s)) := by ring_nf
 607          _ = heatFactor ν (t - s) k := by simp [heatFactor]
 608      -- use the scalar identity to rewrite the smul
 609      calc
 610        (heatFactor ν t k) • (f s)
 611            = ((heatFactor ν t k) * (Real.exp (-(ν * (-kSq k)) * s)))
 612                • (extendByZero (B (u s) (u s)) k) := by
 613                  simpa [f] using
 614                    (smul_smul (heatFactor ν t k) (Real.exp (-(ν * (-kSq k)) * s))
 615                      (extendByZero (B (u s) (u s)) k))
 616        _ = (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
 617              -- rewrite the scalar coefficient
 618              rw [hscalar]
 619    have hinterr :
 620        ∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s)
 621          = ∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) :=
 622      intervalIntegral.integral_congr (μ := MeasureTheory.volume) (a := (0 : ℝ)) (b := t) hEqOn
 623    -- Finish.
 624    -- rewrite the integral using `hinterr`
 625    calc
 626      (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t, f s)
 627          = -∫ s in (0 : ℝ)..t, (heatFactor ν t k) • (f s) := hneg
 628      _ = -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := by
 629            rw [hinterr]
 630
 631  -- Combine.
 632  -- use `hcancel` to rewrite the left-hand side, then apply the rewritten right-hand side
 633  calc
 634    duhamelRemainderOfGalerkin (N := N) ν u t k
 635        = (heatFactor ν t k) • ((Real.exp (-(ν * (-kSq k)) * t)) • duhamelRemainderOfGalerkin (N := N) ν u t k) := by
 636            simpa using hcancel.symm
 637    _ = (heatFactor ν t k) • (-∫ s in (0 : ℝ)..t,
 638          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k)) := by
 639            simpa using hmul
 640    _ = -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (extendByZero (B (u s) (u s)) k) := hRHS
 641
 642/-!
 643## Analytic packaging: dominated convergence for the Duhamel kernel integral
 644
 645To pass the *time-integrated nonlinear forcing* to the limit, we will eventually need a dominated
 646convergence / uniform integrability step. We start by packaging the exact hypotheses needed to apply
 647`intervalIntegral.tendsto_integral_filter_of_dominated_convergence` to the Duhamel kernel integral.
 648
 649This keeps the proof honest (no `sorry`), while making the missing analytic ingredient explicit.
 650-/
 651
 652/-- The Duhamel kernel operator applied to a (Fourier-modewise) forcing trajectory:
 653
 654`(duhamelKernelIntegral ν F)(t,k) = -∫₀ᵗ heatFactor ν (t-s) k • F(s,k) ds`. -/
 655noncomputable def duhamelKernelIntegral (ν : ℝ) (F : ℝ → FourierState2D) : ℝ → FourierState2D :=
 656  fun t k => -∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (F s k)
 657
 658/-- Hypothesis (at fixed `t,k`): the Duhamel-kernel integrands satisfy the assumptions of dominated
 659convergence, so the corresponding interval integrals converge. -/
 660structure DuhamelKernelDominatedConvergenceAt
 661    (ν : ℝ) (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
 662    (t : ℝ) (k : Mode2) where
 663  /-- An `L¹` bound for the integrands on `0..t`. -/
 664  bound : ℝ → ℝ
 665  /-- Strong measurability (eventually in `N`) on the relevant interval. -/
 666  h_meas :
 667    ∀ᶠ N : ℕ in atTop,
 668      MeasureTheory.AEStronglyMeasurable
 669        (fun s : ℝ => (heatFactor ν (t - s) k) • (F_N N s k))
 670        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 671  /-- Dominating bound (eventually in `N`) on the relevant interval. -/
 672  h_bound :
 673    ∀ᶠ N : ℕ in atTop,
 674      ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 675        ‖(heatFactor ν (t - s) k) • (F_N N s k)‖ ≤ bound s
 676  /-- Integrability of the bound. -/
 677  bound_integrable :
 678    IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t
 679  /-- Pointwise (ae on the interval) convergence of the integrands. -/
 680  h_lim :
 681    ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 682      Tendsto (fun N : ℕ => (heatFactor ν (t - s) k) • (F_N N s k)) atTop
 683        (𝓝 ((heatFactor ν (t - s) k) • (F s k)))
 684
 685/-- A more user-facing dominated-convergence hypothesis at fixed `t,k` for the *forcing* itself,
 686without baking in the Duhamel kernel factor. Under `0 ≤ ν` and `0 ≤ t`, this implies
 687`DuhamelKernelDominatedConvergenceAt` because `|heatFactor ν (t-s) k| ≤ 1` on `s ∈ Set.uIoc 0 t`. -/
 688structure ForcingDominatedConvergenceAt
 689    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D) (t : ℝ) (k : Mode2) where
 690  bound : ℝ → ℝ
 691  h_meas :
 692    ∀ᶠ N : ℕ in atTop,
 693      MeasureTheory.AEStronglyMeasurable
 694        (fun s : ℝ => F_N N s k)
 695        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 696  h_bound :
 697    ∀ᶠ N : ℕ in atTop,
 698      ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t → ‖F_N N s k‖ ≤ bound s
 699  bound_integrable :
 700    IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t
 701  h_lim :
 702    ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 703      Tendsto (fun N : ℕ => F_N N s k) atTop (𝓝 (F s k))
 704
 705/-- Heat kernel bound: for `ν ≥ 0` and `τ ≥ 0`, we have `|heatFactor ν τ k| ≤ 1`. -/
 706lemma abs_heatFactor_le_one (ν : ℝ) (hν : 0 ≤ ν) (τ : ℝ) (hτ : 0 ≤ τ) (k : Mode2) :
 707    |heatFactor ν τ k| ≤ 1 := by
 708  -- `heatFactor = exp (-ν * kSq k * τ)` with a nonpositive exponent.
 709  have hkSq : 0 ≤ kSq k := by simp [kSq, add_nonneg, sq_nonneg]
 710  have harg : (-ν * kSq k * τ) ≤ 0 := by
 711    have hprod : 0 ≤ ν * kSq k * τ := mul_nonneg (mul_nonneg hν hkSq) hτ
 712    -- `-x ≤ 0` for `x ≥ 0`
 713    have : -(ν * kSq k * τ) ≤ 0 := neg_nonpos.mpr hprod
 714    simpa [mul_assoc, mul_left_comm, mul_comm] using this
 715  have hle : heatFactor ν τ k ≤ 1 := by
 716    simpa [heatFactor] using (Real.exp_le_one_iff.2 harg)
 717  have hnonneg : 0 ≤ heatFactor ν τ k := (Real.exp_pos _).le
 718  simpa [abs_of_nonneg hnonneg] using hle
 719
 720/-- Convenience constructor: it is often easier to assume pointwise statements (`∀`) rather than
 721almost-everywhere (`∀ᵐ`). This helper upgrades pointwise bounds + convergence to the AE versions
 722required by `ForcingDominatedConvergenceAt`. -/
 723noncomputable def ForcingDominatedConvergenceAt.of_forall
 724    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D) (t : ℝ) (k : Mode2)
 725    (bound : ℝ → ℝ)
 726    (h_meas : ∀ N : ℕ,
 727      MeasureTheory.AEStronglyMeasurable
 728        (fun s : ℝ => F_N N s k)
 729        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)))
 730    (h_bound : ∀ N : ℕ, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t → ‖F_N N s k‖ ≤ bound s)
 731    (bound_integrable : IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t)
 732    (h_lim : ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
 733      Tendsto (fun N : ℕ => F_N N s k) atTop (𝓝 (F s k))) :
 734    ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k :=
 735  { bound := bound
 736    h_meas := Filter.Eventually.of_forall h_meas
 737    h_bound := by
 738      refine Filter.Eventually.of_forall ?_
 739      intro N
 740      exact MeasureTheory.ae_of_all _ (fun s hs => h_bound N s hs)
 741    bound_integrable := bound_integrable
 742    h_lim := by
 743      exact MeasureTheory.ae_of_all _ (fun s hs => h_lim s hs) }
 744
 745/-- Convert a forcing-level dominated convergence hypothesis into the kernel-level one. -/
 746noncomputable def duhamelKernelDominatedConvergenceAt_of_forcing
 747    {ν t : ℝ} (hν : 0 ≤ ν) (ht : 0 ≤ t)
 748    {F_N : ℕ → ℝ → FourierState2D} {F : ℝ → FourierState2D} {k : Mode2}
 749    (hF : ForcingDominatedConvergenceAt F_N F t k) :
 750    DuhamelKernelDominatedConvergenceAt ν F_N F t k := by
 751  classical
 752  refine
 753    { bound := hF.bound
 754      h_meas := ?_
 755      h_bound := ?_
 756      bound_integrable := hF.bound_integrable
 757      h_lim := ?_ }
 758  · -- measurability: `heatFactor( t - s )` is continuous, and `smul` preserves AE-strong measurability
 759    have hheat_meas :
 760        MeasureTheory.AEStronglyMeasurable (fun s : ℝ => heatFactor ν (t - s) k)
 761          (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)) := by
 762      -- continuity in `s`
 763      have hcont : Continuous fun s : ℝ => heatFactor ν (t - s) k := by
 764        -- unfold the scalar kernel and use continuity of `Real.exp`
 765        -- `s ↦ exp (-ν * kSq k * (t - s))`
 766        have hlin : Continuous fun s : ℝ => (-ν * kSq k) * (t - s) := by
 767          exact (continuous_const.mul (continuous_const.sub continuous_id))
 768        simpa [heatFactor, mul_assoc] using (continuous_exp.comp hlin)
 769      exact hcont.aestronglyMeasurable
 770    refine hF.h_meas.mono ?_
 771    intro N hmeasN
 772    exact hheat_meas.smul hmeasN
 773  · -- domination: `|heatFactor| ≤ 1` on `s ∈ uIoc 0 t` (for `t ≥ 0`, `ν ≥ 0`)
 774    refine hF.h_bound.mono ?_
 775    intro N hboundN
 776    filter_upwards [hboundN] with s hsBound
 777    intro hs
 778    have hst : 0 < s ∧ s ≤ t := by
 779      -- unpack membership in the unordered interval
 780      have hs' : min (0 : ℝ) t < s ∧ s ≤ max (0 : ℝ) t := by
 781        simpa [Set.uIoc, Set.mem_Ioc] using hs
 782      simpa [min_eq_left ht, max_eq_right ht] using hs'
 783    have hts : 0 ≤ t - s := sub_nonneg.mpr hst.2
 784    have habs : |heatFactor ν (t - s) k| ≤ 1 :=
 785      abs_heatFactor_le_one ν hν (t - s) hts k
 786    have hx : ‖F_N N s k‖ ≤ hF.bound s := hsBound hs
 787    calc
 788      ‖(heatFactor ν (t - s) k) • (F_N N s k)‖
 789          = |heatFactor ν (t - s) k| * ‖F_N N s k‖ := by
 790              simp [Real.norm_eq_abs, norm_smul]
 791      _ ≤ ‖F_N N s k‖ := by
 792            simpa [one_mul] using (mul_le_of_le_one_left (norm_nonneg _) habs)
 793      _ ≤ hF.bound s := hx
 794  · -- pointwise convergence: multiply by the (fixed-in-`N`) scalar `heatFactor ν (t-s) k`
 795    filter_upwards [hF.h_lim] with s hsLim
 796    intro hs
 797    have hcont : Continuous fun v : VelCoeff => (heatFactor ν (t - s) k) • v := continuous_const_smul _
 798    exact (hcont.tendsto (F s k)).comp (hsLim hs)
 799
 800/-- Under the dominated-convergence hypothesis at `t,k`, the Duhamel-kernel integrals converge. -/
 801theorem tendsto_duhamelKernelIntegral_of_dominated_convergence
 802    (ν : ℝ) (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D) (t : ℝ) (k : Mode2)
 803    (hDC : DuhamelKernelDominatedConvergenceAt ν F_N F t k) :
 804    Tendsto (fun N : ℕ => (duhamelKernelIntegral ν (F_N N) t) k) atTop
 805      (𝓝 ((duhamelKernelIntegral ν F t) k)) := by
 806  -- Apply the dominated convergence theorem for interval integrals.
 807  have hT :
 808      Tendsto
 809          (fun N : ℕ =>
 810            ∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (F_N N s k))
 811          atTop
 812          (𝓝 (∫ s in (0 : ℝ)..t, (heatFactor ν (t - s) k) • (F s k))) := by
 813    simpa using
 814      (intervalIntegral.tendsto_integral_filter_of_dominated_convergence (μ := MeasureTheory.volume)
 815        (a := (0 : ℝ)) (b := t) (l := atTop)
 816        (F := fun N : ℕ => fun s : ℝ => (heatFactor ν (t - s) k) • (F_N N s k))
 817        (f := fun s : ℝ => (heatFactor ν (t - s) k) • (F s k))
 818        (bound := hDC.bound)
 819        (hF_meas := hDC.h_meas)
 820        (h_bound := hDC.h_bound)
 821        (bound_integrable := hDC.bound_integrable)
 822        (h_lim := hDC.h_lim))
 823  -- Move the outer `-` through the limit.
 824  simpa [duhamelKernelIntegral] using hT.neg
 825
 826/-- Galerkin modewise Duhamel identity in kernel form:
 827
 828`û(t,k) = heatFactor ν t k • û(0,k) + duhamelKernelIntegral ν (extendByZero ∘ B(u,u)) (t,k)`.
 829
 830This is just `duhamelRemainderOfGalerkin_kernel` rewritten using the definition of the remainder. -/
 831theorem galerkin_duhamelKernel_identity
 832    {N : ℕ} (ν : ℝ) (B : ConvectionOp N) (u : ℝ → GalerkinState N) (k : Mode2) (t : ℝ)
 833    (hu : ∀ s : ℝ, HasDerivAt u (galerkinNSRHS (N := N) ν B (u s)) s)
 834    (hint :
 835      IntervalIntegrable (fun s : ℝ =>
 836        (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero (B (u s) (u s)) k))
 837        MeasureTheory.volume 0 t) :
 838    (extendByZero (u t) k)
 839      =
 840        (heatFactor ν t k) • (extendByZero (u 0) k)
 841          + (duhamelKernelIntegral ν (fun s : ℝ => extendByZero (B (u s) (u s))) t) k := by
 842  -- Start from the kernel-form remainder identity.
 843  have hR :=
 844    duhamelRemainderOfGalerkin_kernel (N := N) (ν := ν) (B := B) (u := u) (k := k) (t := t) hu hint
 845  -- Unfold the remainder and rearrange.
 846  -- `R(t,k) = û(t,k) - heatFactor(t)•û(0,k)` and `R(t,k) = kernelIntegral(t,k)`.
 847  have :
 848      (extendByZero (u t) k) - (heatFactor ν t k) • (extendByZero (u 0) k)
 849        =
 850          (duhamelKernelIntegral ν (fun s : ℝ => extendByZero (B (u s) (u s))) t) k := by
 851    simpa [duhamelRemainderOfGalerkin, duhamelKernelIntegral] using hR
 852  -- Add the heat term to both sides.
 853  exact (sub_eq_iff_eq_add').1 this
 854
 855/-!
 856## A derived bound: single coefficient ≤ global norm
 857
 858Even before doing any PDE analysis, we can prove a simple but useful fact:
 859the norm of one Fourier coefficient (after zero-extension) is bounded by the
 860global Euclidean norm of the truncated Galerkin state.
 861-/
 862
 863lemma norm_extendByZero_le {N : ℕ} (u : GalerkinState N) (k : Mode2) :
 864    ‖(extendByZero u) k‖ ≤ ‖u‖ := by
 865  classical
 866  by_cases hk : k ∈ modes N
 867  ·
 868    have hext :
 869        (extendByZero u) k =
 870          !₂[u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2)),
 871             u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))] := by
 872      simp [extendByZero, coeffAt, hk]
 873
 874    have hsq_ext :
 875        ‖(extendByZero u) k‖ ^ 2 =
 876          ‖u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2))‖ ^ 2
 877            + ‖u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))‖ ^ 2 := by
 878      -- For `Fin 2`, `EuclideanSpace.norm_sq_eq` expands to the sum of the two coordinate squares.
 879      simp [hext, EuclideanSpace.norm_sq_eq, Fin.sum_univ_two]
 880
 881    have hnorm_u : ‖u‖ ^ 2 = ∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2 := by
 882      simp [EuclideanSpace.norm_sq_eq]
 883
 884    -- The 2-coordinate sum is bounded by the full coordinate sum.
 885    have hcoord_le :
 886        (‖u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2))‖ ^ 2
 887            + ‖u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))‖ ^ 2)
 888          ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := by
 889      let k' : (modes N) := ⟨k, hk⟩
 890      let s : Finset ((modes N) × Fin 2) :=
 891        insert (k', (⟨0, by decide⟩ : Fin 2)) ({(k', (⟨1, by decide⟩ : Fin 2))} : Finset ((modes N) × Fin 2))
 892      have hs : s ⊆ (Finset.univ : Finset ((modes N) × Fin 2)) := by
 893        intro x hx
 894        simp
 895      have hsum :
 896          (‖u (k', (⟨0, by decide⟩ : Fin 2))‖ ^ 2 + ‖u (k', (⟨1, by decide⟩ : Fin 2))‖ ^ 2)
 897            = (∑ kc ∈ s, ‖u kc‖ ^ 2) := by
 898        simp [s]
 899      have hle : (∑ kc ∈ s, ‖u kc‖ ^ 2) ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := by
 900        have hle' :
 901            (∑ kc ∈ s, ‖u kc‖ ^ 2)
 902              ≤ (∑ kc ∈ (Finset.univ : Finset ((modes N) × Fin 2)), ‖u kc‖ ^ 2) := by
 903          refine Finset.sum_le_sum_of_subset_of_nonneg hs ?_
 904          intro kc _hkc _hknot
 905          exact sq_nonneg ‖u kc‖
 906        simpa using hle'
 907      calc
 908        (‖u (k', (⟨0, by decide⟩ : Fin 2))‖ ^ 2 + ‖u (k', (⟨1, by decide⟩ : Fin 2))‖ ^ 2)
 909            = (∑ kc ∈ s, ‖u kc‖ ^ 2) := hsum
 910        _ ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := hle
 911
 912    have hsq_le : ‖(extendByZero u) k‖ ^ 2 ≤ ‖u‖ ^ 2 := by
 913      calc
 914        ‖(extendByZero u) k‖ ^ 2
 915            = (‖u (⟨k, hk⟩, (⟨0, by decide⟩ : Fin 2))‖ ^ 2
 916                + ‖u (⟨k, hk⟩, (⟨1, by decide⟩ : Fin 2))‖ ^ 2) := hsq_ext
 917        _ ≤ (∑ kc : ((modes N) × Fin 2), ‖u kc‖ ^ 2) := hcoord_le
 918        _ = ‖u‖ ^ 2 := by simp [hnorm_u]
 919
 920    exact le_of_sq_le_sq hsq_le (norm_nonneg u)
 921  ·
 922    -- Outside the truncation window the coefficient is zero, so the bound is trivial.
 923    have hnorm : ‖(extendByZero u) k‖ = 0 := by
 924      simp [extendByZero, coeffAt, hk]
 925    simp [hnorm, norm_nonneg u]
 926
 927/-!
 928## Compactness + identification as explicit hypotheses
 929-/
 930
 931/-- Hypothesis: uniform-in-`N` bounds for a *family* of Galerkin trajectories `uN`.
 932
 933In a real proof this would come from:
 934- discrete energy/enstrophy inequalities,
 935- CPM coercivity/dispersion bounds, and
 936- compactness tools (Aubin–Lions / Banach–Alaoglu / etc.).
 937-/
 938structure UniformBoundsHypothesis where
 939  /-- Discrete Galerkin trajectories at each truncation level `N`. -/
 940  uN : (N : ℕ) → ℝ → GalerkinState N
 941  /-- A global (in time, and uniform in `N`) bound. -/
 942  B : ℝ
 943  B_nonneg : 0 ≤ B
 944  /-- Uniform bound: for all `N` and all `t ≥ 0`, `‖uN N t‖ ≤ B`. -/
 945  bound : ∀ N : ℕ, ∀ t ≥ 0, ‖uN N t‖ ≤ B
 946
 947/-- Build `UniformBoundsHypothesis` from the *viscous* Galerkin energy estimate, provided we have
 948an initial uniform bound `‖uN N 0‖ ≤ B` across all truncation levels.
 949-/
 950noncomputable def UniformBoundsHypothesis.ofViscous
 951    (ν : ℝ) (hν : 0 ≤ ν)
 952    (Bop : (N : ℕ) → ConvectionOp N)
 953    (HB : ∀ N : ℕ, EnergySkewHypothesis (Bop N))
 954    (u : (N : ℕ) → ℝ → GalerkinState N)
 955    (hu : ∀ N : ℕ, ∀ t : ℝ, HasDerivAt (u N) (galerkinNSRHS ν (Bop N) ((u N) t)) t)
 956    (B : ℝ) (B_nonneg : 0 ≤ B)
 957    (h0 : ∀ N : ℕ, ‖u N 0‖ ≤ B) :
 958    UniformBoundsHypothesis :=
 959  { uN := u
 960    B := B
 961    B_nonneg := B_nonneg
 962    bound := by
 963      intro N t ht
 964      have hNt : ‖u N t‖ ≤ ‖u N 0‖ :=
 965        viscous_norm_bound_from_initial (N := N) ν hν (Bop N) (HB N) (u N) (hu N) t ht
 966      exact le_trans hNt (h0 N) }
 967
 968/-- The (Galerkin) nonlinear forcing family in full Fourier variables:
 969
 970`F_N(N,s) := extendByZero (Bop N (uN N s) (uN N s))`. -/
 971noncomputable def galerkinForcing (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N) :
 972    ℕ → ℝ → FourierState2D :=
 973  fun N s => extendByZero ((Bop N) (H.uN N s) (H.uN N s))
 974
 975/-- A more concrete, user-facing hypothesis for dominated convergence of the *Galerkin forcing*
 976`galerkinForcing H Bop`, expressed directly in terms of:
 977
 978- measurability of the forcing modes,
 979- an integrable dominating function on each time interval `[0,t]`, and
 980- pointwise convergence of forcing modes.
 981
 982This packages exactly what you need to build `ForcingDominatedConvergenceAt` for the Galerkin forcing. -/
 983structure GalerkinForcingDominatedConvergenceHypothesis
 984    (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N) where
 985  /-- Limiting forcing in full Fourier variables. -/
 986  F : ℝ → FourierState2D
 987  /-- Dominating `L¹` bound, allowed to depend on `(t,k)`. -/
 988  bound : ℝ → Mode2 → ℝ → ℝ
 989  /-- Integrability of the dominating bound on each interval `0..t` (for `t ≥ 0`). -/
 990  bound_integrable : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
 991    IntervalIntegrable (bound t k) MeasureTheory.volume (0 : ℝ) t
 992  /-- Strong measurability (in `s`) of each forcing mode on `0..t` (for `t ≥ 0`). -/
 993  meas : ∀ N : ℕ, ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
 994    MeasureTheory.AEStronglyMeasurable
 995      (fun s : ℝ => (galerkinForcing H Bop N s) k)
 996      (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 997  /-- Pointwise domination by the integrable bound on `0..t` (for `t ≥ 0`). -/
 998  dom : ∀ N : ℕ, ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
 999    ‖(galerkinForcing H Bop N s) k‖ ≤ bound t k s
1000  /-- Pointwise convergence of forcing modes on `0..t` (for `t ≥ 0`). -/
1001  lim : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
1002    Tendsto (fun N : ℕ => (galerkinForcing H Bop N s) k) atTop (𝓝 ((F s) k))
1003
1004namespace GalerkinForcingDominatedConvergenceHypothesis
1005
1006/-- Build `ForcingDominatedConvergenceAt` for the Galerkin forcing from the more concrete hypothesis
1007`GalerkinForcingDominatedConvergenceHypothesis`. -/
1008noncomputable def forcingDCTAt
1009    {H : UniformBoundsHypothesis} {Bop : (N : ℕ) → ConvectionOp N}
1010    (hF : GalerkinForcingDominatedConvergenceHypothesis H Bop)
1011    (t : ℝ) (ht : 0 ≤ t) (k : Mode2) :
1012    ForcingDominatedConvergenceAt (F_N := galerkinForcing H Bop) (F := hF.F) t k :=
1013  ForcingDominatedConvergenceAt.of_forall (F_N := galerkinForcing H Bop) (F := hF.F) (t := t) (k := k)
1014    (bound := hF.bound t k)
1015    (h_meas := by intro N; exact hF.meas N t ht k)
1016    (h_bound := by intro N s hs; exact hF.dom N t ht k s hs)
1017    (bound_integrable := hF.bound_integrable t ht k)
1018    (h_lim := by intro s hs; exact hF.lim t ht k s hs)
1019
1020/-- If each Galerkin trajectory `uN N` is continuous and each `Bop N` is continuous as a map
1021`(u,v) ↦ Bop N u v`, then each forcing mode `s ↦ (galerkinForcing H Bop N s) k` is continuous (hence
1022AE-strongly measurable on any finite interval). -/
1023theorem aestronglyMeasurable_galerkinForcing_mode_of_continuous
1024    (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N)
1025    (hBcont : ∀ N : ℕ,
1026      Continuous (fun p : GalerkinState N × GalerkinState N => (Bop N) p.1 p.2))
1027    (hucont : ∀ N : ℕ, Continuous (H.uN N))
1028    (N : ℕ) (t : ℝ) (_ht : 0 ≤ t) (k : Mode2) :
1029    MeasureTheory.AEStronglyMeasurable
1030      (fun s : ℝ => (galerkinForcing H Bop N s) k)
1031      (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)) := by
1032  -- Continuity of `s ↦ Bop N (uN N s) (uN N s)`.
1033  have hpair : Continuous fun s : ℝ => (H.uN N s, H.uN N s) := by
1034    -- build continuity from `ContinuousAt.prodMk`
1035    refine continuous_iff_continuousAt.2 ?_
1036    intro s
1037    simpa using
1038      (ContinuousAt.prodMk (x := s) ((hucont N).continuousAt) ((hucont N).continuousAt))
1039  have hB : Continuous fun s : ℝ => (Bop N) (H.uN N s) (H.uN N s) :=
1040    (hBcont N).comp hpair
1041  -- Apply the continuous linear map `u ↦ (extendByZero u) k`.
1042  let L : GalerkinState N →L[ℝ] VelCoeff :=
1043    (ContinuousLinearMap.proj k).comp (extendByZeroCLM (N := N))
1044  have hL : Continuous fun u : GalerkinState N => L u := L.continuous
1045  have hcoeff : Continuous fun s : ℝ => (galerkinForcing H Bop N s) k := by
1046    -- unfold back to `extendByZero` + evaluation at `k`
1047    simpa [galerkinForcing, L, extendByZeroCLM] using hL.comp hB
1048  exact hcoeff.aestronglyMeasurable
1049
1050/-- Sufficient condition: a **uniform norm bound** on the convection term plus the uniform-in-time
1051bound `‖uN‖ ≤ B` yields an integrable domination for every forcing mode.
1052
1053This discharges the `bound_integrable` and `dom` fields of `GalerkinForcingDominatedConvergenceHypothesis`,
1054leaving only measurability + pointwise forcing convergence as hypotheses. -/
1055noncomputable def of_convectionNormBound
1056    (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N)
1057    (C : ℝ) (hC : 0 ≤ C)
1058    (hB : ∀ N : ℕ, ∀ u : GalerkinState N, ‖(Bop N u u)‖ ≤ C * ‖u‖ ^ 2)
1059    (F : ℝ → FourierState2D)
1060    (meas : ∀ N : ℕ, ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
1061      MeasureTheory.AEStronglyMeasurable
1062        (fun s : ℝ => (galerkinForcing H Bop N s) k)
1063        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)))
1064    (lim : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
1065      Tendsto (fun N : ℕ => (galerkinForcing H Bop N s) k) atTop (𝓝 ((F s) k))) :
1066    GalerkinForcingDominatedConvergenceHypothesis H Bop :=
1067by
1068  classical
1069  refine
1070    { F := F
1071      bound := fun _t _k _s => C * H.B ^ 2
1072      bound_integrable := by
1073        intro t _ht k
1074        -- constant function is interval integrable on any finite interval
1075        simp
1076      meas := meas
1077      dom := ?_
1078      lim := lim }
1079  intro N t ht k s hs
1080  -- from `s ∈ uIoc 0 t` and `0 ≤ t`, we have `0 < s` hence `0 ≤ s`.
1081  have hs' : 0 < s ∧ s ≤ t := by
1082    have hs'' : min (0 : ℝ) t < s ∧ s ≤ max (0 : ℝ) t := by
1083      simpa [Set.uIoc, Set.mem_Ioc] using hs
1084    simpa [min_eq_left ht, max_eq_right ht] using hs''
1085  have hs0 : 0 ≤ s := le_of_lt hs'.1
1086
1087  -- uniform bound on `uN`
1088  have hu : ‖H.uN N s‖ ≤ H.B := H.bound N s hs0
1089
1090  -- square the bound: `‖u‖^2 ≤ B^2`
1091  have hu_sq : ‖H.uN N s‖ ^ 2 ≤ H.B ^ 2 := by
1092    have : ‖H.uN N s‖ * ‖H.uN N s‖ ≤ H.B * H.B :=
1093      mul_le_mul hu hu (norm_nonneg _) H.B_nonneg
1094    simpa [pow_two] using this
1095
1096  -- control the Galerkin nonlinearity in norm, then pass to a single Fourier coefficient
1097  have hBuu : ‖(Bop N (H.uN N s) (H.uN N s))‖ ≤ C * ‖H.uN N s‖ ^ 2 :=
1098    hB N (H.uN N s)
1099  have hBuu' : ‖(Bop N (H.uN N s) (H.uN N s))‖ ≤ C * H.B ^ 2 :=
1100    le_trans hBuu (mul_le_mul_of_nonneg_left hu_sq hC)
1101  have hcoeff :
1102      ‖(galerkinForcing H Bop N s) k‖ ≤ C * H.B ^ 2 := by
1103    have h1 :
1104        ‖(galerkinForcing H Bop N s) k‖ ≤ ‖(Bop N (H.uN N s) (H.uN N s))‖ := by
1105      simpa [galerkinForcing] using
1106        (norm_extendByZero_le (u := (Bop N (H.uN N s) (H.uN N s))) (k := k))
1107    exact le_trans h1 hBuu'
1108  simpa using hcoeff
1109
1110/-- Combine `of_convectionNormBound` with continuity assumptions to discharge measurability of the
1111Galerkin forcing modes automatically. -/
1112noncomputable def of_convectionNormBound_of_continuous
1113    (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N)
1114    (C : ℝ) (hC : 0 ≤ C)
1115    (hB : ∀ N : ℕ, ∀ u : GalerkinState N, ‖(Bop N u u)‖ ≤ C * ‖u‖ ^ 2)
1116    (hBcont : ∀ N : ℕ,
1117      Continuous (fun p : GalerkinState N × GalerkinState N => (Bop N) p.1 p.2))
1118    (hucont : ∀ N : ℕ, Continuous (H.uN N))
1119    (F : ℝ → FourierState2D)
1120    (lim : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
1121      Tendsto (fun N : ℕ => (galerkinForcing H Bop N s) k) atTop (𝓝 ((F s) k))) :
1122    GalerkinForcingDominatedConvergenceHypothesis H Bop :=
1123  of_convectionNormBound (H := H) (Bop := Bop) (C := C) hC (hB := hB) (F := F)
1124    (meas := by
1125      intro N t ht k
1126      exact aestronglyMeasurable_galerkinForcing_mode_of_continuous (H := H) (Bop := Bop)
1127        (hBcont := hBcont) (hucont := hucont) N t ht k)
1128    (lim := lim)
1129
1130end GalerkinForcingDominatedConvergenceHypothesis
1131
1132/-- Hypothesis: existence of a limit Fourier trajectory and convergence from the approximants. -/
1133structure ConvergenceHypothesis (H : UniformBoundsHypothesis) where
1134  /-- Candidate limit (time → full Fourier coefficients). -/
1135  u : ℝ → FourierState2D
1136  /-- Pointwise (mode-by-mode) convergence of the zero-extended Galerkin coefficients. -/
1137  converges : ∀ t : ℝ, ∀ k : Mode2,
1138    Tendsto (fun N : ℕ => (extendByZero (H.uN N t)) k) atTop (𝓝 ((u t) k))
1139
1140namespace ConvergenceHypothesis
1141
1142/-- Derived fact: if the approximants are uniformly bounded in the Galerkin norm for `t ≥ 0`,
1143then the limit coefficients inherit the same bound (by closedness of `closedBall`). -/
1144theorem coeff_bound_of_uniformBounds {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1145    ∀ t ≥ 0, ∀ k : Mode2, ‖(HC.u t) k‖ ≤ H.B := by
1146  intro t ht k
1147  -- Put every approximant coefficient inside the closed ball of radius `B`.
1148  have hmem :
1149      ∀ N : ℕ, (extendByZero (H.uN N t) k) ∈ Metric.closedBall (0 : VelCoeff) H.B := by
1150    intro N
1151    have h1 : ‖(extendByZero (H.uN N t)) k‖ ≤ ‖H.uN N t‖ :=
1152      norm_extendByZero_le (u := H.uN N t) (k := k)
1153    have h2 : ‖H.uN N t‖ ≤ H.B := H.bound N t ht
1154    have h3 : ‖(extendByZero (H.uN N t)) k‖ ≤ H.B := le_trans h1 h2
1155    -- `Metric.mem_closedBall` is `dist ≤ radius`, and `dist x 0 = ‖x‖`.
1156    simpa [Metric.mem_closedBall, dist_zero_right] using h3
1157
1158  have hmem_event :
1159      (∀ᶠ N : ℕ in atTop, (extendByZero (H.uN N t) k) ∈ Metric.closedBall (0 : VelCoeff) H.B) :=
1160    Filter.Eventually.of_forall hmem
1161
1162  have hlim_mem :
1163      (HC.u t) k ∈ Metric.closedBall (0 : VelCoeff) H.B :=
1164    IsClosed.mem_of_tendsto (b := atTop) Metric.isClosed_closedBall (HC.converges t k) hmem_event
1165
1166  have : dist ((HC.u t) k) (0 : VelCoeff) ≤ H.B :=
1167    (Metric.mem_closedBall).1 hlim_mem
1168
1169  simpa [dist_zero_right] using this
1170
1171/-- If the approximants satisfy the (Fourier) divergence constraint at a fixed `t,k`, then so does
1172the limit coefficient (by continuity + uniqueness of limits in `ℝ`). -/
1173theorem divConstraint_eq_zero_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1174    (t : ℝ) (k : Mode2)
1175    (hDF : ∀ N : ℕ, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1176    divConstraint k ((HC.u t) k) = 0 := by
1177  -- Push convergence through the continuous map `divConstraint k`.
1178  have hT :
1179      Tendsto (fun N : ℕ => divConstraint k ((extendByZero (H.uN N t)) k)) atTop
1180        (𝓝 (divConstraint k ((HC.u t) k))) := by
1181    have hcont : Continuous (fun v : VelCoeff => divConstraint k v) := divConstraint_continuous k
1182    have hcontT :
1183        Tendsto (fun v : VelCoeff => divConstraint k v) (𝓝 ((HC.u t) k))
1184          (𝓝 (divConstraint k ((HC.u t) k))) :=
1185      hcont.tendsto ((HC.u t) k)
1186    exact hcontT.comp (HC.converges t k)
1187
1188  -- The sequence is constantly 0 by assumption.
1189  have heq : (fun N : ℕ => divConstraint k ((extendByZero (H.uN N t)) k)) = fun _ : ℕ => (0 : ℝ) := by
1190    funext N
1191    simpa using (hDF N)
1192
1193  have hT0 : Tendsto (fun _ : ℕ => (0 : ℝ)) atTop (𝓝 (divConstraint k ((HC.u t) k))) := by
1194    simpa [heq] using hT
1195  have hconst : Tendsto (fun _ : ℕ => (0 : ℝ)) atTop (𝓝 (0 : ℝ)) := tendsto_const_nhds
1196
1197  exact tendsto_nhds_unique hT0 hconst
1198
1199/-- Divergence-free passes to the limit under modewise convergence, assuming each approximant is
1200divergence-free (in the Fourier-side sense) at every time. -/
1201theorem divFree_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1202    (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1203    IsDivergenceFreeTraj HC.u := by
1204  intro t k
1205  exact divConstraint_eq_zero_of_forall (HC := HC) (t := t) (k := k) (hDF := fun N => hDF N t k)
1206
1207/-- Mild Stokes/heat identity passes to the limit under modewise convergence,
1208assuming it holds for every approximant (modewise, for `t ≥ 0`). -/
1209theorem stokesMild_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1210    (hMild :
1211      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1212        (extendByZero (H.uN N t) k) = (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) :
1213    IsStokesMildTraj ν HC.u := by
1214  intro t ht k
1215  -- convergence at time t and at time 0
1216  have hconv_t : Tendsto (fun N : ℕ => extendByZero (H.uN N t) k) atTop (nhds ((HC.u t) k)) :=
1217    HC.converges t k
1218  have hconv_0 : Tendsto (fun N : ℕ => extendByZero (H.uN N 0) k) atTop (nhds ((HC.u 0) k)) :=
1219    HC.converges 0 k
1220  -- push convergence at time 0 through the continuous map `v ↦ heatFactor • v`
1221  have hsmul :
1222      Tendsto (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) atTop
1223        (nhds ((heatFactor ν t k) • ((HC.u 0) k))) := by
1224    have hcont : Continuous fun v : VelCoeff => (heatFactor ν t k) • v := continuous_const_smul _
1225    exact (hcont.tendsto ((HC.u 0) k)).comp hconv_0
1226  -- but the two sequences are equal for all N (by hypothesis), hence have the same limit
1227  have hEq :
1228      (fun N : ℕ => extendByZero (H.uN N t) k)
1229        =ᶠ[atTop] (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) := by
1230    refine Filter.Eventually.of_forall ?_
1231    intro N
1232    exact hMild N t ht k
1233  -- uniqueness of limits in a T2 space
1234  have : (HC.u t) k = (heatFactor ν t k) • ((HC.u 0) k) :=
1235    tendsto_nhds_unique_of_eventuallyEq hconv_t hsmul hEq
1236  simpa using this
1237
1238/-- Duhamel-remainder identity passes to the limit under modewise convergence,
1239assuming it holds for every approximant with remainders `D_N` that converge modewise. -/
1240theorem nsDuhamel_of_forall {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1241    (D_N : ℕ → ℝ → FourierState2D) (D : ℝ → FourierState2D)
1242    (hD : ∀ t : ℝ, ∀ k : Mode2,
1243      Tendsto (fun N : ℕ => (D_N N t) k) atTop (nhds ((D t) k)))
1244    (hId :
1245      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1246        (extendByZero (H.uN N t) k) =
1247          (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (D_N N t) k) :
1248    IsNSDuhamelTraj ν D HC.u := by
1249  intro t ht k
1250  -- convergence of the main trajectory at time `t` and at time `0`
1251  have hconv_t : Tendsto (fun N : ℕ => extendByZero (H.uN N t) k) atTop (nhds ((HC.u t) k)) :=
1252    HC.converges t k
1253  have hconv_0 : Tendsto (fun N : ℕ => extendByZero (H.uN N 0) k) atTop (nhds ((HC.u 0) k)) :=
1254    HC.converges 0 k
1255  -- convergence of the remainder term
1256  have hconv_D : Tendsto (fun N : ℕ => (D_N N t) k) atTop (nhds ((D t) k)) :=
1257    hD t k
1258  -- push convergence at time 0 through the continuous map `v ↦ heatFactor • v`
1259  have hsmul :
1260      Tendsto (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) atTop
1261        (nhds ((heatFactor ν t k) • ((HC.u 0) k))) := by
1262    have hcont : Continuous fun v : VelCoeff => (heatFactor ν t k) • v := continuous_const_smul _
1263    exact (hcont.tendsto ((HC.u 0) k)).comp hconv_0
1264  -- combine the smul part and the remainder part
1265  have hsum :
1266      Tendsto (fun N : ℕ =>
1267        (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (D_N N t) k) atTop
1268          (nhds ((heatFactor ν t k) • ((HC.u 0) k) + (D t) k)) :=
1269    hsmul.add hconv_D
1270  -- the identity holds for every N, hence the two sequences are eventually equal
1271  have hEq :
1272      (fun N : ℕ => extendByZero (H.uN N t) k)
1273        =ᶠ[atTop] (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (D_N N t) k) := by
1274    refine Filter.Eventually.of_forall ?_
1275    intro N
1276    exact hId N t ht k
1277  -- uniqueness of limits in a T2 space
1278  have :
1279      (HC.u t) k = (heatFactor ν t k) • ((HC.u 0) k) + (D t) k :=
1280    tendsto_nhds_unique_of_eventuallyEq hconv_t hsum hEq
1281  simpa [IsNSDuhamelTraj] using this
1282
1283/-- Convenience wrapper around `nsDuhamel_of_forall` when the remainder terms are defined as Duhamel
1284kernel integrals and convergence is supplied via dominated convergence (hypothesis-level). -/
1285theorem nsDuhamel_of_forall_kernelIntegral {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1286    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1287    (hDC : ∀ t : ℝ, ∀ k : Mode2, DuhamelKernelDominatedConvergenceAt ν F_N F t k)
1288    (hId :
1289      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1290        (extendByZero (H.uN N t) k) =
1291          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1292            + (duhamelKernelIntegral ν (F_N N) t) k) :
1293    IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) HC.u := by
1294  have hD :
1295      ∀ t : ℝ, ∀ k : Mode2,
1296        Tendsto (fun N : ℕ => (duhamelKernelIntegral ν (F_N N) t) k) atTop
1297          (nhds (((duhamelKernelIntegral ν F) t) k)) := by
1298    intro t k
1299    exact tendsto_duhamelKernelIntegral_of_dominated_convergence (ν := ν) (F_N := F_N) (F := F) (t := t) (k := k)
1300      (hDC t k)
1301  exact
1302    nsDuhamel_of_forall (HC := HC) (ν := ν)
1303      (D_N := fun N => duhamelKernelIntegral ν (F_N N)) (D := duhamelKernelIntegral ν F)
1304      (hD := hD) (hId := hId)
1305
1306/-- Variant of `nsDuhamel_of_forall_kernelIntegral` that assumes dominated convergence only for the
1307*forcing* (not the kernel integrand), plus `0 ≤ ν` and `t ≥ 0` to control the kernel factor. -/
1308theorem nsDuhamel_of_forall_kernelIntegral_of_forcing {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1309    (ν : ℝ) (hν : 0 ≤ ν)
1310    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1311    (hF :
1312      ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k)
1313    (hId :
1314      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1315        (extendByZero (H.uN N t) k) =
1316          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1317            + (duhamelKernelIntegral ν (F_N N) t) k) :
1318    IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) HC.u := by
1319  intro t ht k
1320  -- convergence of the main trajectory at time `t` and at time `0`
1321  have hconv_t : Tendsto (fun N : ℕ => extendByZero (H.uN N t) k) atTop (nhds ((HC.u t) k)) :=
1322    HC.converges t k
1323  have hconv_0 : Tendsto (fun N : ℕ => extendByZero (H.uN N 0) k) atTop (nhds ((HC.u 0) k)) :=
1324    HC.converges 0 k
1325  -- convergence of the kernel-integral remainder at time `t` (from forcing-level DCT)
1326  have hconv_D :
1327      Tendsto (fun N : ℕ => (duhamelKernelIntegral ν (F_N N) t) k) atTop
1328        (nhds (((duhamelKernelIntegral ν F) t) k)) := by
1329    have hDC : DuhamelKernelDominatedConvergenceAt ν F_N F t k :=
1330      duhamelKernelDominatedConvergenceAt_of_forcing (ν := ν) (t := t) hν ht (hF t ht k)
1331    exact
1332      tendsto_duhamelKernelIntegral_of_dominated_convergence (ν := ν) (F_N := F_N) (F := F) (t := t) (k := k)
1333        hDC
1334  -- push convergence at time 0 through the continuous map `v ↦ heatFactor • v`
1335  have hsmul :
1336      Tendsto (fun N : ℕ => (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) atTop
1337        (nhds ((heatFactor ν t k) • ((HC.u 0) k))) := by
1338    have hcont : Continuous fun v : VelCoeff => (heatFactor ν t k) • v := continuous_const_smul _
1339    exact (hcont.tendsto ((HC.u 0) k)).comp hconv_0
1340  -- combine the smul part and the remainder part
1341  have hsum :
1342      Tendsto (fun N : ℕ =>
1343        (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (duhamelKernelIntegral ν (F_N N) t) k) atTop
1344          (nhds ((heatFactor ν t k) • ((HC.u 0) k) + ((duhamelKernelIntegral ν F) t) k)) :=
1345    hsmul.add hconv_D
1346  -- the identity holds for every N, hence the two sequences are eventually equal
1347  have hEq :
1348      (fun N : ℕ => extendByZero (H.uN N t) k)
1349        =ᶠ[atTop]
1350          (fun N : ℕ =>
1351            (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (duhamelKernelIntegral ν (F_N N) t) k) := by
1352    refine Filter.Eventually.of_forall ?_
1353    intro N
1354    exact hId N t ht k
1355  -- uniqueness of limits in a T2 space
1356  have :
1357      (HC.u t) k = (heatFactor ν t k) • ((HC.u 0) k) + ((duhamelKernelIntegral ν F) t) k :=
1358    tendsto_nhds_unique_of_eventuallyEq hconv_t hsum hEq
1359  simpa [IsNSDuhamelTraj] using this
1360
1361end ConvergenceHypothesis
1362
1363/-- Convenience constructor: if each coefficient sequence is *eventually equal* to the corresponding
1364limit coefficient, then it tends to that limit. -/
1365noncomputable def ConvergenceHypothesis.ofEventuallyEq
1366    (H : UniformBoundsHypothesis)
1367    (u : ℝ → FourierState2D)
1368    (heq :
1369      ∀ t : ℝ, ∀ k : Mode2,
1370        (fun N : ℕ => (extendByZero (H.uN N t)) k) =ᶠ[atTop] (fun _ : ℕ => (u t) k)) :
1371    ConvergenceHypothesis H :=
1372  { u := u
1373    converges := by
1374      intro t k
1375      have hconst : Tendsto (fun _ : ℕ => (u t) k) atTop (𝓝 ((u t) k)) :=
1376        tendsto_const_nhds
1377      exact (tendsto_congr' (heq t k)).2 hconst }
1378
1379/-- Hypothesis: the limit object satisfies the intended PDE identity (kept abstract here). -/
1380structure IdentificationHypothesis {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) where
1381  /-- A (later: concrete) solution concept for 2D Navier–Stokes on the torus. -/
1382  IsSolution : (ℝ → FourierState2D) → Prop
1383  /-- Proof that the limit trajectory satisfies the chosen solution concept. -/
1384  isSolution : IsSolution HC.u
1385
1386namespace IdentificationHypothesis
1387
1388/-- Trivial identification constructor: choose `IsSolution := True`. -/
1389def trivial {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1390    IdentificationHypothesis HC :=
1391  { IsSolution := fun _ => True
1392    isSolution := by trivial }
1393
1394/-- Concrete (but still minimal) identification: define `IsSolution u` to mean the limit coefficients
1395are uniformly bounded by the Galerkin bound `H.B` for `t ≥ 0`.
1396
1397This is **provable** from `UniformBoundsHypothesis` + modewise convergence (no extra analytic input),
1398via `ConvergenceHypothesis.coeff_bound_of_uniformBounds`.
1399-/
1400def coeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) :
1401    IdentificationHypothesis HC :=
1402  { IsSolution := fun u => ∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B
1403    isSolution := by
1404      intro t ht k
1405      simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k) }
1406
1407/-- Identification constructor: coefficient bound + divergence-free (Fourier-side).
1408
1409The coefficient bound part is proved from `UniformBoundsHypothesis` + convergence.
1410The divergence-free part is proved from the extra assumption that *each approximant* is divergence-free.
1411-/
1412def divFreeCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1413    (hDF : ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2, divConstraint k ((extendByZero (H.uN N t)) k) = 0) :
1414    IdentificationHypothesis HC :=
1415  { IsSolution := fun u =>
1416      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsDivergenceFreeTraj u
1417    isSolution := by
1418      refine ⟨?_, ?_⟩
1419      · intro t ht k
1420        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1421      · intro t k
1422        exact ConvergenceHypothesis.divConstraint_eq_zero_of_forall (HC := HC) (t := t) (k := k)
1423          (hDF := fun N => hDF N t k) }
1424
1425/-- Identification constructor: coefficient bound + (linear) Stokes/heat mild identity.
1426
1427The bound part is proved from `UniformBoundsHypothesis` + convergence.
1428The mild Stokes identity is proved from the extra assumption that it holds for every approximant. -/
1429def stokesMildCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1430    (hMild :
1431      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1432        (extendByZero (H.uN N t) k) = (heatFactor ν t k) • (extendByZero (H.uN N 0) k)) :
1433    IdentificationHypothesis HC :=
1434  { IsSolution := fun u =>
1435      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsStokesMildTraj ν u
1436    isSolution := by
1437      refine ⟨?_, ?_⟩
1438      · intro t ht k
1439        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1440      · exact ConvergenceHypothesis.stokesMild_of_forall (HC := HC) (ν := ν) hMild }
1441
1442/-- Identification constructor: coefficient bound + a first nonlinear (Duhamel-style) remainder identity.
1443
1444The coefficient bound part is proved from `UniformBoundsHypothesis` + convergence.
1445The Duhamel-remainder identity is proved from the extra assumptions:
1446
1447- each approximant satisfies `extendByZero uN(t,k) = heatFactor • extendByZero uN(0,k) + D_N(t,k)`, and
1448- `D_N(t,k) → D(t,k)` modewise.
1449
1450In later milestones, `D_N` will be instantiated as an actual time-integrated nonlinear forcing term. -/
1451def nsDuhamelCoeffBound {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1452    (D_N : ℕ → ℝ → FourierState2D) (D : ℝ → FourierState2D)
1453    (hD : ∀ t : ℝ, ∀ k : Mode2,
1454      Tendsto (fun N : ℕ => (D_N N t) k) atTop (nhds ((D t) k)))
1455    (hId :
1456      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1457        (extendByZero (H.uN N t) k) =
1458          (heatFactor ν t k) • (extendByZero (H.uN N 0) k) + (D_N N t) k) :
1459    IdentificationHypothesis HC :=
1460  { IsSolution := fun u =>
1461      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν D u
1462    isSolution := by
1463      refine ⟨?_, ?_⟩
1464      · intro t ht k
1465        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1466      · exact ConvergenceHypothesis.nsDuhamel_of_forall (HC := HC) (ν := ν) (D_N := D_N) (D := D) hD hId }
1467
1468/-- Identification constructor: coefficient bound + Duhamel remainder identity where the remainder is
1469defined as a **kernel integral** of a forcing term, and convergence of the kernel integrals is
1470packaged via `DuhamelKernelDominatedConvergenceAt`. -/
1471def nsDuhamelCoeffBound_kernelIntegral {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1472    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1473    (hDC : ∀ t : ℝ, ∀ k : Mode2, DuhamelKernelDominatedConvergenceAt ν F_N F t k)
1474    (hId :
1475      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1476        (extendByZero (H.uN N t) k) =
1477          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1478            + (duhamelKernelIntegral ν (F_N N) t) k) :
1479    IdentificationHypothesis HC :=
1480  { IsSolution := fun u =>
1481      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) u
1482    isSolution := by
1483      refine ⟨?_, ?_⟩
1484      · intro t ht k
1485        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1486      · exact
1487          ConvergenceHypothesis.nsDuhamel_of_forall_kernelIntegral (HC := HC) (ν := ν)
1488            (F_N := F_N) (F := F) hDC hId }
1489
1490/-- Same as `nsDuhamelCoeffBound_kernelIntegral`, but assumes dominated convergence at the **forcing**
1491level (not the kernel integrand), plus `0 ≤ ν`. -/
1492def nsDuhamelCoeffBound_kernelIntegral_of_forcing {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1493    (ν : ℝ) (hν : 0 ≤ ν)
1494    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1495    (hF :
1496      ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k)
1497    (hId :
1498      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1499        (extendByZero (H.uN N t) k) =
1500          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1501            + (duhamelKernelIntegral ν (F_N N) t) k) :
1502    IdentificationHypothesis HC :=
1503  { IsSolution := fun u =>
1504      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) u
1505    isSolution := by
1506      refine ⟨?_, ?_⟩
1507      · intro t ht k
1508        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1509      · exact
1510          ConvergenceHypothesis.nsDuhamel_of_forall_kernelIntegral_of_forcing (HC := HC)
1511            (ν := ν) hν (F_N := F_N) (F := F) hF hId }
1512
1513/-- Identification constructor: a specialization of `nsDuhamelCoeffBound_kernelIntegral` where the
1514forcing family is the **actual Galerkin nonlinearity** `extendByZero (B(u_N,u_N))`. The Duhamel
1515identity for each approximant is discharged by `galerkin_duhamelKernel_identity`; the remaining
1516analytic ingredient is the dominated-convergence hypothesis `hDC`. -/
1517def nsDuhamelCoeffBound_galerkinKernel {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H) (ν : ℝ)
1518    (Bop : (N : ℕ) → ConvectionOp N)
1519    (hu :
1520      ∀ N : ℕ, ∀ s : ℝ,
1521        HasDerivAt (H.uN N) (galerkinNSRHS (N := N) ν (Bop N) (H.uN N s)) s)
1522    (hint :
1523      ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
1524        IntervalIntegrable (fun s : ℝ =>
1525          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero ((Bop N) (H.uN N s) (H.uN N s)) k))
1526          MeasureTheory.volume 0 t)
1527    (F : ℝ → FourierState2D)
1528    (hDC :
1529      ∀ t : ℝ, ∀ k : Mode2,
1530        DuhamelKernelDominatedConvergenceAt ν
1531          (fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (H.uN N s) (H.uN N s))) F t k) :
1532    IdentificationHypothesis HC := by
1533  -- Define the forcing family from the Galerkin nonlinearity.
1534  let F_N : ℕ → ℝ → FourierState2D :=
1535    fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (H.uN N s) (H.uN N s))
1536  -- The approximant Duhamel identity follows from the Galerkin kernel lemma.
1537  have hId' :
1538      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1539        (extendByZero (H.uN N t) k) =
1540          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1541            + (duhamelKernelIntegral ν (F_N N) t) k := by
1542    intro N t _ht k
1543    -- `galerkin_duhamelKernel_identity` does not require `t ≥ 0`, but we only need it on that domain.
1544    simpa [F_N] using
1545      (galerkin_duhamelKernel_identity (N := N) (ν := ν) (B := Bop N) (u := H.uN N) (k := k) (t := t)
1546        (hu := fun s => hu N s) (hint := hint N t k))
1547  -- Reduce to the kernel-integral constructor.
1548  refine nsDuhamelCoeffBound_kernelIntegral (HC := HC) (ν := ν) (F_N := F_N) (F := F) ?_ hId'
1549  intro t k
1550  simpa [F_N] using hDC t k
1551
1552/-- Same as `nsDuhamelCoeffBound_galerkinKernel`, but assumes dominated convergence at the **forcing**
1553level (not the kernel integrand), plus `0 ≤ ν`. -/
1554def nsDuhamelCoeffBound_galerkinKernel_of_forcing {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1555    (ν : ℝ) (hν : 0 ≤ ν)
1556    (Bop : (N : ℕ) → ConvectionOp N)
1557    (hu :
1558      ∀ N : ℕ, ∀ s : ℝ,
1559        HasDerivAt (H.uN N) (galerkinNSRHS (N := N) ν (Bop N) (H.uN N s)) s)
1560    (hint :
1561      ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
1562        IntervalIntegrable (fun s : ℝ =>
1563          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero ((Bop N) (H.uN N s) (H.uN N s)) k))
1564          MeasureTheory.volume 0 t)
1565    (F : ℝ → FourierState2D)
1566    (hF :
1567      ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
1568        ForcingDominatedConvergenceAt
1569          (F_N := fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (H.uN N s) (H.uN N s)))
1570          (F := F) t k) :
1571    IdentificationHypothesis HC := by
1572  -- Define the forcing family from the Galerkin nonlinearity.
1573  let F_N : ℕ → ℝ → FourierState2D :=
1574    fun N : ℕ => fun s : ℝ => extendByZero ((Bop N) (H.uN N s) (H.uN N s))
1575  -- The approximant Duhamel identity follows from the Galerkin kernel lemma.
1576  have hId' :
1577      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1578        (extendByZero (H.uN N t) k) =
1579          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1580            + (duhamelKernelIntegral ν (F_N N) t) k := by
1581    intro N t _ht k
1582    simpa [F_N] using
1583      (galerkin_duhamelKernel_identity (N := N) (ν := ν) (B := Bop N) (u := H.uN N) (k := k) (t := t)
1584        (hu := fun s => hu N s) (hint := hint N t k))
1585  -- Reduce to the forcing-level kernel-integral constructor.
1586  refine
1587    nsDuhamelCoeffBound_kernelIntegral_of_forcing (HC := HC) (ν := ν) hν (F_N := F_N) (F := F) ?_ hId'
1588  intro t ht k
1589  simpa [F_N] using hF t ht k
1590
1591/-- Same as `nsDuhamelCoeffBound_galerkinKernel_of_forcing`, but takes the more concrete hypothesis
1592`GalerkinForcingDominatedConvergenceHypothesis` for the Galerkin forcing modes. -/
1593def nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1594    (ν : ℝ) (hν : 0 ≤ ν)
1595    (Bop : (N : ℕ) → ConvectionOp N)
1596    (hu :
1597      ∀ N : ℕ, ∀ s : ℝ,
1598        HasDerivAt (H.uN N) (galerkinNSRHS (N := N) ν (Bop N) (H.uN N s)) s)
1599    (hint :
1600      ∀ N : ℕ, ∀ t : ℝ, ∀ k : Mode2,
1601        IntervalIntegrable (fun s : ℝ =>
1602          (Real.exp (-(ν * (-kSq k)) * s)) • (extendByZero ((Bop N) (H.uN N s) (H.uN N s)) k))
1603          MeasureTheory.volume 0 t)
1604    (hForce : GalerkinForcingDominatedConvergenceHypothesis H Bop) :
1605    IdentificationHypothesis HC := by
1606  refine
1607    nsDuhamelCoeffBound_galerkinKernel_of_forcing (HC := HC) (ν := ν) hν (Bop := Bop) (hu := hu) (hint := hint)
1608      (F := hForce.F) ?_
1609  intro t ht k
1610  -- unpack the forcing-level DCT hypothesis for the Galerkin forcing modes
1611  simpa [galerkinForcing] using (GalerkinForcingDominatedConvergenceHypothesis.forcingDCTAt (hF := hForce) t ht k)
1612
1613end IdentificationHypothesis
1614
1615/-!
1616## The milestone theorem: “uniform bounds + convergence + identification ⇒ continuum solution”
1617
1618At this stage the theorem returns the packaged limit object together with its claimed properties.
1619-/
1620
1621theorem continuum_limit_exists
1622    (H : UniformBoundsHypothesis)
1623    (HC : ConvergenceHypothesis H)
1624    (HI : IdentificationHypothesis HC) :
1625    ∃ u : ℝ → FourierState2D,
1626      (∀ t : ℝ, ∀ k : Mode2, Tendsto (fun N : ℕ => (extendByZero (H.uN N t)) k) atTop (𝓝 ((u t) k)))
1627        ∧ HI.IsSolution u
1628        ∧ (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) := by
1629  refine ⟨HC.u, HC.converges, ?_, ?_⟩
1630  · simpa using HI.isSolution
1631  · intro t ht k
1632    simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1633
1634end ContinuumLimit2D
1635
1636end IndisputableMonolith.ClassicalBridge.Fluids
1637