ConvectionOp
ConvectionOp supplies the type of the abstract bilinear convection operator on the finite-dimensional Galerkin state space for each truncation level N in a 2D Fourier-mode model of incompressible flow. Researchers working on discrete Navier-Stokes approximations cite this when isolating the nonlinear term for energy estimates and passage to the continuum limit. The definition is a direct type abbreviation to the space of maps from pairs of states to states.
claimFor each natural number $N$, let $V_N$ denote the Euclidean space of velocity coefficients indexed by the truncated modes and the two spatial components. The convection operator is then any map $B_N : V_N → V_N → V_N$.
background
The module constructs a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus. Its goal is a concrete discrete state space together with the basic algebraic energy identity for the inviscid case, keeping the nonlinear term abstract as a bilinear operator $B$ while requiring only the inner-product property that ensures energy conservation. Upstream, GalerkinState $N$ is the abbreviation EuclideanSpace ℝ ((modes $N$) × Fin 2), which assembles the velocity coefficients for each retained mode and each of the two components.
proof idea
The declaration is a one-line type definition that directly identifies ConvectionOp $N$ with the function space GalerkinState $N$ → GalerkinState $N$ → GalerkinState $N$. No lemmas or tactics are invoked; the abbreviation serves as a reusable type for the projected nonlinearity.
why it matters in Recognition Science
This definition supplies the abstract handle on the nonlinearity that is instantiated throughout the continuum-limit arguments. It is used by galerkinForcing to build the forcing term from any Galerkin trajectory, by the Duhamel identities to express the integral remainder, and by the dominated-convergence hypotheses that control passage to the continuum. In the Recognition framework it supports the bridge from discrete energy identities to the full Navier-Stokes equations while preserving the algebraic structure needed for later steps.
scope and limits
- Does not supply an explicit Fourier-convolution formula for the operator.
- Does not include the Leray projection onto divergence-free fields.
- Does not enforce the skew-symmetry condition that the inner product of B(u,u) with u vanishes.
- Does not assert continuity or boundedness of the operator.
formal statement (Lean)
77def ConvectionOp (N : ℕ) : Type :=
proof body
Definition body.
78 GalerkinState N → GalerkinState N → GalerkinState N
79
80/-- Discrete Navier–Stokes RHS: u' = νΔu - B(u,u). -/
used by (26)
-
aestronglyMeasurable_galerkinForcing_mode_of_continuous -
duhamelRemainderOfGalerkin_integratingFactor -
duhamelRemainderOfGalerkin_kernel -
forcingDCTAt -
galerkin_duhamelKernel_identity -
galerkinForcing -
GalerkinForcingDominatedConvergenceHypothesis -
galerkinNS_hasDerivAt_duhamelRemainder_mode -
galerkinNS_hasDerivAt_extendByZero_mode -
nsDuhamelCoeffBound_galerkinKernel -
nsDuhamelCoeffBound_galerkinKernel_of_forcing -
nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp -
of_convectionNormBound -
of_convectionNormBound_of_continuous -
UniformBoundsHypothesis -
EnergySkewHypothesis -
galerkinNSRHS -
inviscid_energy_deriv_zero -
viscous_energy_antitone -
viscous_energy_bound_from_initial -
viscous_energy_deriv_le_zero -
viscous_energy_deriv_nonpos -
viscous_norm_bound_from_initial -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcing -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound_galerkinKernel_of_forcingHyp