viscous_energy_bound3
plain-language theorem explainer
This theorem shows that the discrete kinetic energy of any solution to the 3D spectral Galerkin Navier-Stokes ODE remains bounded by its initial value for nonnegative viscosity. Analysts deriving a priori estimates for finite-mode truncations of incompressible flow would cite it when controlling L2 growth. The argument is a direct specialization of the antitone property of the energy functional along trajectories.
Claim. Let $E(t) := (1/2) |u(t)|^2$ be the discrete energy of a curve $u : R to R^M$ in the finite Galerkin space that satisfies the ODE $u'(t) = nu Delta u(t) - B(u(t),u(t))$, where the bilinear operator $B$ obeys the skew condition $langle B(v,v), v rangle = 0$ for every state $v$. Then $E(t) le E(0)$ for all $t ge 0$.
background
The module constructs a Fourier-Galerkin truncation of the 3D Navier-Stokes equations on the torus, retaining modes with wave numbers in [-N,N]^3. GalerkinState3 is the Euclidean space of velocity coefficients indexed by these modes times the three components. discreteEnergy3 extracts half the squared Euclidean norm of the coefficient vector. ConvectionOp3 supplies the projected bilinear nonlinearity, while EnergySkewHypothesis3 records the algebraic identity that this term is orthogonal to the velocity. The right-hand side galerkinNSRHS3 assembles the viscous Laplacian term scaled by nu together with the negative convection term. The present result depends on the upstream theorem viscous_energy_antitone3, which already establishes that the energy map is antitone along any solution of the ODE.
proof idea
The proof is a one-line wrapper that applies viscous_energy_antitone3 to obtain the antitone property of t |-> discreteEnergy3(u t) and then restricts the resulting inequality to the interval t >= 0.
why it matters
viscous_norm_bound3 invokes the same hypotheses to conclude that the Euclidean norm of u(t) is likewise bounded by its initial value. The declaration supplies the energy monotonicity step required in the Galerkin approximation analysis of RS_NavierStokes_BKM.tex section 4. In the Recognition Science setting it anchors the discrete energy control that precedes enstrophy estimates in the sub-Kolmogorov framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.