tendsto_duhamelKernelIntegral_of_dominated_convergence
plain-language theorem explainer
This result establishes pointwise convergence of the Duhamel kernel integrals for sequences of Galerkin approximations to the continuum Fourier state in 2D fluid models. Analysts working on the passage from finite-dimensional truncations to the Navier-Stokes continuum limit would cite it when justifying interchange of limits and integrals in the Duhamel formula. The proof applies the interval integral dominated convergence theorem from Mathlib and then negates the result to match the kernel definition.
Claim. Let $ν ∈ ℝ$, let $F_N : ℕ → ℝ →$ (full infinite Fourier coefficient state for 2D velocity on $𝕋²$), $F : ℝ →$ (full infinite Fourier coefficient state) the limit trajectory, $t ∈ ℝ$, and $k$ a mode. Under the hypothesis supplying an $L¹$ bound on the integrands, eventual strong measurability, integrability of the bound, and pointwise convergence of the integrands, we have $lim_{N→∞} (duhamelKernelIntegral ν (F_N N) t) k = (duhamelKernelIntegral ν F t) k$.
background
FourierState2D is the full (infinite) Fourier coefficient state for a 2D velocity field on $𝕋²$, obtained by extending truncated Galerkin states by zero outside the truncation window. DuhamelKernelDominatedConvergenceAt is the structure at fixed $t,k$ that packages an $L¹$ bound, eventual strong measurability of the integrands, integrability of the bound, and pointwise convergence of the integrands to the limit trajectory. The definition duhamelKernelIntegral ν F is the operator sending $t,k$ to $-∫_0^t$ heatFactor ν $(t-s)$ k • $F(s,k)$ ds. The module ContinuumLimit2D (Milestone M5) packages the analytic compactness steps from finite Galerkin approximations to a continuum limit object as explicit hypotheses rather than axioms.
proof idea
The proof first applies the Mathlib lemma intervalIntegral.tendsto_integral_filter_of_dominated_convergence to the family of integrands (heatFactor ν $(t-s)$ k) • $(F_N N s k)$, feeding the bound, measurability, integrability and limit hypotheses directly from the dominated-convergence structure. It then uses simpa with the definition of duhamelKernelIntegral to move the leading minus sign through the limit.
why it matters
This theorem is invoked by nsDuhamel_of_forall_kernelIntegral and its forcing variant, which wrap the Navier-Stokes Duhamel identity when remainders are expressed as kernel integrals and convergence is supplied via dominated convergence. It fills an identification step in the M5 pipeline of ContinuumLimit2D that makes the dependency graph from Galerkin truncations to the continuum object explicit. No direct connection to the Recognition Science forcing chain or phi-ladder appears here; the result remains inside the classical bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.