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

DuhamelKernelDominatedConvergenceAt

show as:
view Lean formalization →

DuhamelKernelDominatedConvergenceAt encodes the dominated-convergence hypotheses for the heat-weighted Duhamel integrands at fixed time t and Fourier mode k. Analysts justifying passage from Galerkin approximations to the continuum 2D Navier-Stokes solution cite it to interchange limit and integral. The declaration is a structure that bundles an integrable dominating function, eventual strong measurability, domination, integrability, and pointwise convergence of the integrands.

claimFix viscosity parameter $ν$, sequence of forcing maps $F_N : ℕ → ℝ →$ Fourier coefficient state, limiting forcing $F : ℝ →$ Fourier coefficient state, time $t$, and Fourier mode $k$. The structure asserts an integrable bound function $b : ℝ → ℝ$, eventual strong measurability of the map $s ↦$ (heat factor $ν (t-s) k$) · ($F_N N s k$), domination of these terms by $b(s)$ almost everywhere on $(0,t)$, integrability of $b$ over $[0,t]$, and almost-everywhere pointwise convergence of the sequence to the corresponding limit integrand.

background

The ContinuumLimit2D module packages the analytic steps required to pass from finite Galerkin truncations to an infinite Fourier coefficient state for 2D velocity fields on the torus. Fourier coefficient states are maps from Fourier modes (integer pairs) to velocity coefficients; the heat factor at mode $k$ is the real exponential damping $exp(-ν |k|^2 t)$ that solves the linear Stokes evolution modewise.

proof idea

This is a structure definition that collects the five fields required by the dominated convergence theorem: an $L^1$ bound, eventual AEStronglyMeasurable, the domination inequality almost everywhere, IntervalIntegrable of the bound, and almost-everywhere pointwise convergence of the heat-weighted approximants.

why it matters in Recognition Science

It supplies the analytic hypothesis for nsDuhamelCoeffBound_kernelIntegral and the related identification theorems that connect Galerkin solutions to the continuum object. These feed directly into the regularity results in Regularity2D. Within the Recognition framework it contributes to milestone M5 by making the dominated-convergence step for the Duhamel kernel explicit rather than axiomatic.

scope and limits

formal statement (Lean)

 660structure DuhamelKernelDominatedConvergenceAt
 661    (ν : ℝ) (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D)
 662    (t : ℝ) (k : Mode2) where
 663  /-- An `L¹` bound for the integrands on `0..t`. -/
 664  bound : ℝ → ℝ
 665  /-- Strong measurability (eventually in `N`) on the relevant interval. -/
 666  h_meas :
 667    ∀ᶠ N : ℕ in atTop,
 668      MeasureTheory.AEStronglyMeasurable
 669        (fun s : ℝ => (heatFactor ν (t - s) k) • (F_N N s k))
 670        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 671  /-- Dominating bound (eventually in `N`) on the relevant interval. -/
 672  h_bound :
 673    ∀ᶠ N : ℕ in atTop,
 674      ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 675        ‖(heatFactor ν (t - s) k) • (F_N N s k)‖ ≤ bound s
 676  /-- Integrability of the bound. -/
 677  bound_integrable :
 678    IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t
 679  /-- Pointwise (ae on the interval) convergence of the integrands. -/
 680  h_lim :
 681    ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 682      Tendsto (fun N : ℕ => (heatFactor ν (t - s) k) • (F_N N s k)) atTop
 683        (𝓝 ((heatFactor ν (t - s) k) • (F s k)))
 684
 685/-- A more user-facing dominated-convergence hypothesis at fixed `t,k` for the *forcing* itself,
 686without baking in the Duhamel kernel factor. Under `0 ≤ ν` and `0 ≤ t`, this implies
 687`DuhamelKernelDominatedConvergenceAt` because `|heatFactor ν (t-s) k| ≤ 1` on `s ∈ Set.uIoc 0 t`. -/

used by (8)

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

depends on (21)

Lean names referenced from this declaration's body.