viscous_energy_antitone3
plain-language theorem explainer
The declaration establishes that the discrete energy of a trajectory satisfying the 3D Galerkin-truncated Navier-Stokes system is a non-increasing function of time whenever viscosity is non-negative. Spectral fluid dynamicists working on finite-mode approximations would cite it to obtain a priori bounds before passing to the continuum limit. The argument is a one-line wrapper that invokes the general criterion for antitone functions of a differentiable map once the energy derivative and its non-positivity have been supplied by sibling lemmas.
Claim. Let $N$ be a natural number, let $ν ≥ 0$, let $B$ be a bilinear convection operator on the $N$-truncated Fourier space satisfying $⟨B(u,u),u⟩=0$ for all $u$, and let $u:ℝ→$ (truncated velocity field) satisfy $u'(t)=νΔu(t)-B(u(t),u(t))$. Then the map $t↦½‖u(t)‖² is antitone.
background
The 3D Galerkin module truncates the incompressible Navier-Stokes equations on the torus T³ to Fourier modes with wave numbers in [-N,N]³. GalerkinState3 is the Euclidean space of coefficient vectors indexed by these modes times the three velocity components. ConvectionOp3 is the bilinear map that realizes the projected nonlinearity, while EnergySkewHypothesis3 records the algebraic identity that makes this term energy-neutral. The discrete energy is defined as half the squared Euclidean norm of the coefficient vector. The right-hand side of the ODE is ν times the spectral Laplacian (multiplication by -k²) minus the convection term.
proof idea
The proof is a one-line wrapper that applies antitone_of_hasDerivAt_nonpos to the composition of discreteEnergy3 with the trajectory u. It supplies the explicit derivative of the energy along solutions from viscous_energy_deriv3 and the fact that this derivative is non-positive from viscous_energy_nonpos3.
why it matters
The result is the monotonicity step required by viscous_energy_bound3, which concludes that discrete energy at any later time is at most the initial value. It sits inside the Galerkin approximation developed in RS_NavierStokes_BKM.tex §4 and supplies the energy-dissipation identity needed to control the spectral enstrophy in the discrete sub-Kolmogorov setting. The parent theorem viscous_energy_bound3 directly consumes this antitone property to close the a-priori bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.