IsDivergenceFreeTraj

formal source

 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