laplacianCoeff_inner_self_nonpos
plain-language theorem explainer
The inner product of any Galerkin velocity field with its Fourier Laplacian is non-positive. Researchers deriving uniform energy bounds for truncated 2D Navier-Stokes cite this algebraic fact to control the viscous term. The proof expands the inner product as a finite sum over modes, factors each term as (-k²) times a square, and applies nonpositivity of the multiplier together with nonnegativity of squares.
Claim. For any natural number $N$ and Galerkin state $u$ (velocity coefficients indexed by truncated 2D Fourier modes and two components), the real inner product satisfies $⟨u, Δu⟩_ℝ ≤ 0$, where the discrete Laplacian $Δ$ multiplies the coefficient at mode $k$ by $-|k|^2$.
background
The module constructs a finite-dimensional Fourier-truncated model for 2D incompressible Navier-Stokes on the torus, with the explicit goal of obtaining algebraic energy identities before any continuum limit. GalerkinState N is the Euclidean space of real coefficients indexed by the finite set (modes N) × Fin 2, where modes N collects integer pairs with max(|k1|,|k2|) ≤ N. The operator laplacianCoeff multiplies each coefficient at mode k by -kSq(k), and kSq(k) is defined as k1² + k2². This lemma supplies the sign of the dissipation term that appears in the viscous energy derivative.
proof idea
The tactic proof first rewrites the inner product via PiLp.inner_apply and the definition of laplacianCoeff to obtain an explicit sum over (modes N) × Fin 2 of u_kc * (-kSq(kc.1) * u_kc). It then applies Finset.sum_nonpos. For each summand it establishes kSq ≥ 0 by add_nonneg and sq_nonneg, deduces -kSq ≤ 0 by linarith, notes u_kc² ≥ 0 by mul_self_nonneg, rewrites the product by ring, and concludes nonpositivity by mul_nonpos_of_nonpos_of_nonneg.
why it matters
The lemma is invoked directly by viscous_energy_deriv_nonpos and viscous_energy_antitone to obtain the nonpositive derivative of discreteEnergy under positive viscosity. It therefore supplies the algebraic input for uniform energy bounds in the Galerkin truncation, exactly as described in the module's section on viscous energy dissipation. Within the Recognition framework this step closes the discrete energy identity needed for the classical bridge before any passage to the continuum or to the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.