divConstraint_continuous
plain-language theorem explainer
divConstraint_continuous establishes that the Fourier divergence map for each fixed mode is continuous on the space of velocity coefficients. Researchers passing Galerkin truncations to continuum fluid limits cite it to justify interchanging limits with the divergence-free condition. The proof is a short tactic script that composes coordinate projection continuity with the algebraic operations in the divergence expression.
Claim. For each fixed mode $k=(k_1,k_2)∈ℤ²$, the map $v↦k_1 v_1 + k_2 v_2$ from velocity coefficients $v∈ℝ²$ to $ℝ$ is continuous.
background
The module ContinuumLimit2D develops a Lean-checkable pipeline from finite 2D Galerkin approximations to a continuum Fourier state, keeping compactness steps as explicit hypotheses. Mode2 is the type of 2D Fourier modes $(k_1,k_2)$. VelCoeff realizes velocity coefficients as the Euclidean space $ℝ²$. The definition divConstraint k v computes the Fourier-side divergence $k_1 v_1 + k_2 v_2$ for a single mode.
proof idea
The proof obtains continuity of the two coordinate projections on VelCoeff via PiLp.continuous_apply, then combines them with continuity of constant multiplication and addition before simplifying with the definition of divConstraint.
why it matters
This lemma is invoked by divConstraint_eq_zero_of_forall, which transfers the divergence-free property from approximants to the limit coefficient under the convergence hypothesis. It supplies an analytic step in the ClassicalBridge.Fluids pipeline for passing discrete models to continuum PDE statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.