IsNSDuhamelTraj
plain-language theorem explainer
Analysts formalizing the continuum limit of 2D Navier-Stokes Galerkin schemes cite the Duhamel remainder predicate when they need a modewise mild formulation that augments the linear heat evolution with a nonlinear forcing term D. The predicate requires that each Fourier coefficient of the trajectory at time t equals the heat-damped initial coefficient plus the remainder coefficient. It is introduced by direct transcription of the integral form into pointwise equalities on modes.
Claim. A map $u : ℝ → (ℤ² → ℂ)$ satisfies the Duhamel form with remainder $D$ and viscosity $ν$ when ∀ $t ≥ 0$, ∀ $k ∈ ℤ²$, $u(t)(k) = exp(-ν |k|² t) · u(0)(k) + D(t)(k)$.
background
The module ContinuumLimit2D develops a Lean pipeline for passing Galerkin approximations of 2D incompressible fluids to a continuum Fourier state. FourierState2D denotes the space of all functions assigning a complex velocity coefficient to each integer mode pair on the torus. The heatFactor supplies the explicit multiplier exp(-ν |k|² t) solving the linear viscous term.
proof idea
The declaration is a definition that directly asserts the modewise equality combining the heat evolution operator with the remainder. No lemmas are applied; it simply packages the target identity that downstream identification theorems verify in the limit.
why it matters
Downstream theorems nsDuhamelCoeffBound and nsDuhamel_of_forall use this predicate as the target property that the limiting trajectory must satisfy. It completes the mild-form interface in the M5 continuum-limit milestone, allowing the graph of hypotheses to be discharged step by step. The construction keeps the analytic identification steps explicit rather than axiomatic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.