IsDivergenceFree

formal source

 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)