viscous_energy_antitone
plain-language theorem explainer
The theorem shows that the discrete kinetic energy of any differentiable solution to the viscous Galerkin Navier-Stokes system is a non-increasing function of time. Researchers deriving a priori bounds for finite-mode fluid approximations would cite it when controlling dissipation. The argument is a direct application of the general antitone criterion for maps with non-positive derivative, after verifying the explicit energy derivative via the viscous inner-product term.
Claim. Let $B$ be an abstract convection operator on the Galerkin state space satisfying the skew-symmetry condition $⟨B(u,u),u⟩=0$ for every state $u$. Suppose $u:ℝ→$ Galerkin states is differentiable and obeys the evolution $u'=νΔu-B(u,u)$ with viscosity coefficient $ν≥0$. Then the map $t↦½‖u(t)‖²$ is antitone.
background
The module builds a finite-dimensional Fourier-truncated model for 2D incompressible Navier-Stokes on the torus. GalerkinState N is the Euclidean space of velocity coefficients indexed by the first N modes and two components. ConvectionOp N is an abstract bilinear map standing in for the projected nonlinearity, while EnergySkewHypothesis B encodes the single algebraic relation $⟨B(u,u),u⟩=0$ that yields exact energy conservation when viscosity is absent. Discrete energy is defined as half the squared Euclidean norm of the state vector. The evolution right-hand side is $ν$ times the Laplacian coefficient (multiplication by $-|k|²$ on each mode) minus B(u,u).
proof idea
The term proof invokes the general calculus fact antitone_of_hasDerivAt_nonpos on the composite map t↦discreteEnergy(u t). It supplies the explicit derivative $ν⟪u, laplacianCoeff u⟫$ by calling viscous_energy_deriv_le_zero. The inner product is shown non-positive by laplacianCoeff_inner_self_nonpos, after which mul_nonpos_of_nonneg_of_nonpos combines the sign of $ν$ with the sign of the inner product to conclude the derivative is ≤0.
why it matters
The result supplies the monotonicity step required by the downstream theorem viscous_energy_bound_from_initial, which concludes that energy at any positive time is at most the initial value. Within the M1 milestone it completes the viscous dissipation identity after the inviscid conservation identity encoded by EnergySkewHypothesis. It prepares later work on energy cascades in the truncated system, while the continuum limit and the explicit Fourier realization of B remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.