lemma
proved
tactic proof
divConstraint_continuous
show as:
view Lean formalization →
Last generation error: xAI API error (429): The model is currently at capacity due to high demand. Please try again in a few minutes. For guaranteed processing and availability, please request Provisioned Throughput: https://docs.x.ai/developers/advanced-api-usage/provisioned-throughput
formal statement (Lean)
138lemma divConstraint_continuous (k : Mode2) : Continuous fun v : VelCoeff => divConstraint k v := by
proof body
Tactic-mode proof.
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}`. -/