laplacianCoeff
plain-language theorem explainer
The definition applies the Fourier Laplacian to a truncated Galerkin velocity field by scaling each mode coefficient by its negative squared wavenumber. Researchers deriving dissipation estimates for discrete Navier-Stokes models cite it when analyzing the viscous term. The implementation is a direct pointwise multiplication inside the Euclidean space of coefficients.
Claim. For truncation level $N$ and Galerkin state $u$, the operator returns the state whose coefficient at mode $k$ is $-|k|^2 u(k)$, where $|k|^2 = k_1^2 + k_2^2$.
background
The Galerkin2D module builds a finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus. GalerkinState is the Euclidean space of real coefficients indexed by the finite set of modes up to $N$ together with the two velocity components. kSq supplies the squared wavenumber for each Mode2 pair of integers.
proof idea
One-line definition that constructs the output state via WithLp.toLp 2 applied to the pointwise map sending each coefficient index kc to (-kSq kc.1) times the input coefficient.
why it matters
It supplies the linear term inside galerkinNSRHS and is invoked by laplacianCoeff_inner_self_nonpos, viscous_energy_deriv_nonpos, viscous_energy_antitone and viscous_energy_deriv_le_zero to obtain the sign of the energy derivative under positive viscosity. The definition completes the algebraic setup for the M1 discrete energy identities before the continuum limit is taken in ContinuumLimit2D.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.