pith. machine review for the scientific record. sign in
def definition def or abbrev high

nsDuhamelCoeffBound_kernelIntegral_of_forcing

show as:
view Lean formalization →

Constructs an identification hypothesis asserting that a limit Fourier trajectory satisfies the Navier-Stokes Duhamel equation under forcing-dominated convergence. Researchers formalizing 2D continuum limits from Galerkin approximations cite it when the forcing family satisfies the dominated-convergence condition at each mode. The definition assembles the required solution record by extracting the uniform coefficient bound and applying the specialized Duhamel lemma for kernel integrals.

claimLet $H$ be a uniform bounds hypothesis on a family of Galerkin trajectories $u_N$ with global bound $B$, and let $HC$ be a convergence hypothesis from the zero-extended approximants to a candidate limit trajectory $u$. For viscosity parameter $ν ≥ 0$, forcing families $F_N$ and $F$, and given that the forcing converges in the dominated sense at every $t ≥ 0$ and mode $k$ together with the Duhamel identity holding for each approximant, the construction yields an identification hypothesis for $HC$ whose solution property is the conjunction of the inherited bound on $u$ and the Navier-Stokes Duhamel trajectory condition driven by the Duhamel integral of $F$.

background

UniformBoundsHypothesis packages a family of Galerkin states $u_N$ together with a uniform bound $B$ such that the norm of each approximant remains ≤ $B$ for all truncation levels $N$ and all times $t ≥ 0$. ConvergenceHypothesis $HC$ supplies the candidate limit trajectory $u : ℝ →$ FourierState2D and asserts pointwise convergence of the zero-extended coefficients to those of $u$ at every mode. FourierState2D is the space of all maps from Mode2 to velocity coefficients for 2D fields on the torus; extendByZero embeds a truncated Galerkin state into this space by padding with zeros outside the retained modes. ForcingDominatedConvergenceAt encodes the dominated-convergence data for the forcing terms themselves at fixed $t$ and $k$; under $ν ≥ 0$ this transfers to the Duhamel kernel integrands because the heat factor is bounded by 1. The module ContinuumLimit2D develops a Lean-checkable pipeline shape for passing from finite-dimensional 2D Galerkin approximations to a continuum Fourier limit object, packaging the analytic compactness and identification steps as explicit hypotheses.

proof idea

The definition builds the IdentificationHypothesis record whose IsSolution predicate is the conjunction of the uniform bound on limit coefficients and the IsNSDuhamelTraj property for the Duhamel integral of $F$. The isSolution field is proved by a two-step refinement: the first conjunct is discharged by applying coeff_bound_of_uniformBounds to the convergence hypothesis, while the second conjunct is obtained directly from the lemma nsDuhamel_of_forall_kernelIntegral_of_forcing instantiated with the supplied forcing convergence data $hF$ and the approximant Duhamel identities $hId$.

why it matters in Recognition Science

This definition supplies the forcing-level specialization of the identification constructor, feeding directly into nsDuhamelCoeffBound_galerkinKernel_of_forcing which replaces the abstract forcing family by the actual Galerkin nonlinearity. It advances the M5 milestone of the ContinuumLimit2D pipeline by making the passage from approximants to the limit trajectory explicit once forcing-dominated convergence is assumed. In the Recognition Science framework it provides a rigorous classical-bridge interface for the incompressible Navier-Stokes equations before any quantization or cost-algebra steps are applied.

scope and limits

formal statement (Lean)

1492def nsDuhamelCoeffBound_kernelIntegral_of_forcing {H : UniformBoundsHypothesis} (HC : ConvergenceHypothesis H)
1493    (ν : ℝ) (hν : 0 ≤ ν)
1494    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
1495    (hF :
1496      ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ForcingDominatedConvergenceAt (F_N := F_N) (F := F) t k)

proof body

Definition body.

1497    (hId :
1498      ∀ N : ℕ, ∀ t ≥ 0, ∀ k : Mode2,
1499        (extendByZero (H.uN N t) k) =
1500          (heatFactor ν t k) • (extendByZero (H.uN N 0) k)
1501            + (duhamelKernelIntegral ν (F_N N) t) k) :
1502    IdentificationHypothesis HC :=
1503  { IsSolution := fun u =>
1504      (∀ t ≥ 0, ∀ k : Mode2, ‖(u t) k‖ ≤ H.B) ∧ IsNSDuhamelTraj ν (duhamelKernelIntegral ν F) u
1505    isSolution := by
1506      refine ⟨?_, ?_⟩
1507      · intro t ht k
1508        simpa using (ConvergenceHypothesis.coeff_bound_of_uniformBounds (HC := HC) t ht k)
1509      · exact
1510          ConvergenceHypothesis.nsDuhamel_of_forall_kernelIntegral_of_forcing (HC := HC)
1511            (ν := ν) hν (F_N := F_N) (F := F) hF hId }
1512
1513/-- Identification constructor: a specialization of `nsDuhamelCoeffBound_kernelIntegral` where the
1514forcing family is the **actual Galerkin nonlinearity** `extendByZero (B(u_N,u_N))`. The Duhamel
1515identity for each approximant is discharged by `galerkin_duhamelKernel_identity`; the remaining
1516analytic ingredient is the dominated-convergence hypothesis `hDC`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (33)

Lean names referenced from this declaration's body.

… and 3 more