discreteEnergy3
plain-language theorem explainer
discreteEnergy3 defines the kinetic energy of a 3D Galerkin truncation state as half the squared Euclidean norm of its coefficient vector. Analysts deriving energy estimates for spectral Navier-Stokes approximations cite this definition when establishing conservation and dissipation. The implementation is a direct one-line scaling of the vector norm on the finite-dimensional state space.
Claim. For a state $u$ in the 3D Galerkin truncation space at level $N$, the discrete energy is $E(u) = (1/2) |u|^2$, where the norm is the Euclidean norm on the coefficient space over the truncated Fourier modes.
background
The module extends the 2D Galerkin truncation to three dimensions on the torus $T^3$ with modes in $[-N,N]^3$. GalerkinState3 N is the Euclidean space over the product of the finite mode set (modes3 N) and the three velocity components, equipped with the standard inner product and norm. This finite-dimensional setting represents velocity fields via Fourier coefficients while preserving the energy identity for the projected nonlinearity.
proof idea
The definition is a one-line wrapper that applies the squared Euclidean norm to the input Galerkin state and scales the result by one half.
why it matters
This definition supplies the energy functional used by the downstream theorems inviscid_energy_deriv_zero3, viscous_energy_antitone3, viscous_energy_bound3, viscous_energy_deriv3 and viscous_norm_bound3. Those results establish energy conservation without viscosity and monotonic decrease under positive viscosity, matching the Galerkin approximation described in RS_NavierStokes_BKM.tex §4 and supporting the link to the discrete sub-Kolmogorov framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.