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

ForcingDominatedConvergenceAt

show as:
view Lean formalization →

ForcingDominatedConvergenceAt packages the dominated-convergence hypotheses for a sequence of Galerkin forcing terms F_N at fixed time t and Fourier mode k. Analysts formalizing the passage from finite-dimensional 2D approximations to continuum Navier-Stokes solutions cite it to justify limit interchange in the mild formulation. The declaration is a structure definition that collects eventual strong measurability, an integrable dominating bound, and pointwise convergence of the forcing coefficients on the interval [0,t].

claimLet $F_N : ℕ → ℝ →$ FourierState2D$, $F : ℝ →$ FourierState2D$, $t ∈ ℝ$, $k ∈$ Mode2. The structure consists of a bound $b : ℝ → ℝ$ such that, eventually in $N$, the map $s ↦ F_N(N,s)(k)$ is almost strongly measurable on $[0,t]$, satisfies $‖F_N(N,s)(k)‖ ≤ b(s)$ for almost every $s ∈ [0,t]$, $b$ is integrable over $[0,t]$, and $F_N(N,s)(k) → F(s)(k)$ as $N → ∞$ for almost every $s ∈ [0,t]$. Here FourierState2D denotes the space of all Fourier coefficients indexed by 2D modes and Mode2 the integer lattice points.

background

The ContinuumLimit2D module defines a Lean-checkable pipeline shape for passing from finite-dimensional 2D Galerkin approximations to a continuum limit object. It introduces the infinite Fourier coefficient state and packages analytic compactness steps as explicit hypotheses without axioms or sorrys. FourierState2D is the abbrev Mode2 → VelCoeff for the full Fourier expansion of a 2D velocity field on the torus. Mode2 is the abbrev ℤ × ℤ. The heatFactor is the def exp(−ν ⋅ kSq(k) ⋅ τ) supplying the Stokes decay multiplier. Upstream DuhamelKernelDominatedConvergenceAt is the analogous structure that already multiplies the forcing by the heat kernel.

proof idea

This is a structure definition whose five fields directly record the hypotheses of the dominated convergence theorem applied to the forcing sequence. The fields are bound, eventual AEStronglyMeasurable, the domination inequality almost everywhere, IntervalIntegrable of the bound, and the almost-everywhere pointwise limit. No lemmas or tactics are invoked inside the definition; it functions as a hypothesis carrier.

why it matters in Recognition Science

The structure is converted into DuhamelKernelDominatedConvergenceAt by duhamelKernelDominatedConvergenceAt_of_forcing once 0 ≤ ν and 0 ≤ t are given, using the bound |heatFactor ν (t−s) k| ≤ 1. It is constructed from GalerkinForcingDominatedConvergenceHypothesis via forcingDCTAt and appears in the coefficient bounds nsDuhamelCoeffBound_galerkinKernel_of_forcing and nsDuhamel_of_forall_kernelIntegral_of_forcing. Within the Recognition Science classical bridge at milestone M5 it supplies the forcing-level compactness step that later milestones can replace by proofs, keeping the dependency graph explicit.

scope and limits

formal statement (Lean)

 688structure ForcingDominatedConvergenceAt
 689    (F_N : ℕ → ℝ → FourierState2D) (F : ℝ → FourierState2D) (t : ℝ) (k : Mode2) where
 690  bound : ℝ → ℝ
 691  h_meas :
 692    ∀ᶠ N : ℕ in atTop,
 693      MeasureTheory.AEStronglyMeasurable
 694        (fun s : ℝ => F_N N s k)
 695        (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 696  h_bound :
 697    ∀ᶠ N : ℕ in atTop,
 698      ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t → ‖F_N N s k‖ ≤ bound s
 699  bound_integrable :
 700    IntervalIntegrable bound MeasureTheory.volume (0 : ℝ) t
 701  h_lim :
 702    ∀ᵐ s ∂MeasureTheory.volume, s ∈ Set.uIoc (0 : ℝ) t →
 703      Tendsto (fun N : ℕ => F_N N s k) atTop (𝓝 (F s k))
 704
 705/-- Heat kernel bound: for `ν ≥ 0` and `τ ≥ 0`, we have `|heatFactor ν τ k| ≤ 1`. -/

used by (9)

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

depends on (25)

Lean names referenced from this declaration's body.