ForcingDominatedConvergenceAt
plain-language theorem explainer
ForcingDominatedConvergenceAt packages the dominated-convergence hypotheses for a sequence of forcing maps F_N converging to a limit F at fixed time t and Fourier mode k. Researchers formalizing the continuum limit of 2D Galerkin fluid approximations cite this structure to state forcing-level assumptions cleanly before passing to the Duhamel kernel. The definition assembles four fields: eventual strong measurability on [0,t], an integrable dominating bound, and almost-everywhere pointwise convergence.
Claim. Let $F_N : ℕ → ℝ → (Mode2 → VelCoeff)$ and $F : ℝ → (Mode2 → VelCoeff)$ be families of forcing terms, $t ≥ 0$, and $k$ a Fourier mode. The structure asserts there exists bound : ℝ → ℝ such that, eventually in $N$, the map $s ↦ F_N N s k$ is strongly measurable on the interval $[0,t]$, $‖F_N N s k‖ ≤ bound(s)$ almost everywhere on $[0,t]$, bound is integrable on $[0,t]$, and $F_N N s k → F s k$ almost everywhere on $[0,t]$.
background
The ContinuumLimit2D module (Milestone M5) defines a Lean-checkable pipeline from finite-dimensional 2D Galerkin approximations to a continuum limit object, packaging analytic compactness steps as explicit hypotheses. FourierState2D is the type of full infinite Fourier coefficient states Mode2 → VelCoeff for a 2D velocity field on 𝕋². Mode2 is the type ℤ × ℤ of 2D Fourier modes. The upstream heatFactor supplies the Fourier-side heat/Stokes factor exp(−ν |k|² τ).
proof idea
This is a structure definition that directly assembles the four fields (bound, h_meas, h_bound, bound_integrable, h_lim) required for the forcing-level dominated convergence statement. No lemmas or tactics are invoked inside the definition.
why it matters
ForcingDominatedConvergenceAt is converted to DuhamelKernelDominatedConvergenceAt by duhamelKernelDominatedConvergenceAt_of_forcing under 0 ≤ ν and 0 ≤ t, using the bound |heatFactor ν (t-s) k| ≤ 1. It is instantiated by forcingDCTAt from GalerkinForcingDominatedConvergenceHypothesis and supports the nsDuhamel family of bounds. This advances the explicit packaging of analytic steps in the M5 continuum-limit pipeline for fluids.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.