IsNSDuhamelTraj
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not prove that any trajectory satisfying the predicate solves the Navier-Stokes PDE in the classical sense.
- Does not constrain the growth or integrability of the remainder D.
- Does not incorporate the divergence-free condition on the velocity field.
- Does not address the passage from finite to infinite modes.
- Does not guarantee uniqueness of u given D.
formal statement (Lean)
194def IsNSDuhamelTraj (ν : ℝ) (D : ℝ → FourierState2D) (u : ℝ → FourierState2D) : Prop :=
proof body
Definition body.
195 ∀ t ≥ 0, ∀ k : Mode2, (u t) k = (heatFactor ν t k) • (u 0) k + (D t) k
196
197namespace IsStokesMildTraj
198
199/-- Mild Stokes/heat identity implies the corresponding differential equation (within `t ≥ 0`). -/
used by (10)
-
nsDuhamelCoeffBound -
nsDuhamelCoeffBound_kernelIntegral -
nsDuhamelCoeffBound_kernelIntegral_of_forcing -
nsDuhamel_of_forall -
nsDuhamel_of_forall_kernelIntegral -
nsDuhamel_of_forall_kernelIntegral_of_forcing -
rs_implies_global_regularity_2d_nsDuhamelCoeffBound -
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