viscous_norm_bound_from_initial
plain-language theorem explainer
The theorem establishes an a priori L2 bound for trajectories of the viscous Galerkin Navier-Stokes system on the torus. Analysts working on finite-mode truncations cite it to control coefficient growth before taking continuum limits. The argument invokes the discrete energy inequality and converts it to a norm bound by multiplying through by 2 and applying the square-root monotonicity of the norm on nonnegative reals.
Claim. Let $N$ be a natural number, let $ν ≥ 0$, let $B$ be a convection operator on the space of Galerkin states satisfying the energy-skew condition $⟨B(u,u),u⟩=0$, and let $u:ℝ→$Galerkin state space be a differentiable curve obeying the discrete Navier-Stokes equation $u'=νΔu−B(u,u)$. Then $‖u(t)‖≤‖u(0)‖$ for every $t≥0$.
background
The module builds a finite-dimensional Fourier-truncated model of 2D incompressible Navier-Stokes on the torus. GalerkinState is the Euclidean space of velocity coefficients indexed by the finite set of modes and two components. ConvectionOp abstracts the projected bilinear nonlinearity, while galerkinNSRHS assembles the right-hand side as the viscous Laplacian term minus the convection term. EnergySkewHypothesis encodes the single algebraic identity $⟨B(u,u),u⟩=0$ that guarantees energy conservation when viscosity vanishes. The upstream theorem viscous_energy_bound_from_initial supplies the corresponding bound on the discrete kinetic energy $E(u)=½‖u‖².
proof idea
The tactic proof opens by calling viscous_energy_bound_from_initial to obtain the energy inequality. It rewrites the result via the definition of discreteEnergy to reach ½‖u t‖² ≤ ½‖u 0‖². Multiplication by 2 produces the squared-norm comparison, after which le_of_sq_le_sq together with norm nonnegativity yields the final norm bound.
why it matters
The result populates the uniform bound hypothesis required by UniformBoundsHypothesis in the continuum-limit module. It completes the viscous energy control begun by viscous_energy_bound_from_initial and supplies the basic a priori estimate that later compactness arguments in the Galerkin2D milestone rely upon. Within the classical bridge it furnishes the L2 control that must precede any passage to the continuum Navier-Stokes equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.