divConstraint_continuous
For each fixed 2D Fourier mode the map from velocity coefficient vectors to the scalar divergence value is continuous. Researchers building Galerkin-to-continuum passages for incompressible fluids cite this when transferring the divergence-free condition across limits. The proof extracts the two coordinate projections via PiLp continuity and closes under constant multiplication and addition.
claimFor each fixed mode $k=(k_1,k_2)inmathbb{Z}^2$, the map $vmapsto k_1v_1+k_2v_2$ from $mathbb{R}^2$ to $mathbb{R}$ is continuous.
background
Module ContinuumLimit2D (M5) supplies the pipeline shape that embeds finite Galerkin truncations into an infinite Fourier coefficient state and packages analytic steps as explicit hypotheses. Mode2 is the type of 2D Fourier modes, an integer pair. VelCoeff is the Euclidean 2-space of velocity Fourier coefficients at a mode. divConstraint k v is the real scalar $k_1v_1+k_2v_2$ that encodes the Fourier-side divergence constraint for that mode.
proof idea
The tactic proof first obtains continuity of each coordinate projection on the Euclidean space via PiLp.continuous_apply. It then combines the two projections with constant multiplications and addition, using the algebraic definition of divConstraint to finish.
why it matters in Recognition Science
The lemma is invoked by divConstraint_eq_zero_of_forall, which transfers the divergence-free condition from approximants to the limit coefficient via continuity and uniqueness of limits. This supplies one concrete identification step inside the M5 continuum-limit pipeline and keeps the classical-bridge argument free of extra compactness assumptions beyond modewise convergence.
scope and limits
- Does not establish joint continuity in both mode and coefficient.
- Does not address time dependence or nonlinear convective terms.
- Does not prove existence or uniqueness of continuum solutions.
- Applies only to the linear divergence constraint, not the full Stokes or Navier-Stokes operator.
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}`. -/