of_convectionNormBound_of_continuous
This definition assembles a dominated-convergence hypothesis for the Galerkin forcing term by feeding uniform trajectory bounds together with continuity of the convection operators and trajectories into the base constructor. Analysts working on rigorous passage from finite Galerkin truncations to continuum limits in two-dimensional periodic fluids would cite it. The body is a direct wrapper that supplies the strong-measurability witness from the companion continuity theorem while passing the uniform bound and pointwise limit data unchanged.
claimLet $H$ be a uniform-bounds hypothesis for a family of Galerkin trajectories $u_N$, let $Bop_N$ be a family of convection operators, and let $C$ be a nonnegative constant such that the operator norm of $Bop_N(u,u)$ is at most $C$ times the square of the norm of $u$. Assume each $Bop_N$ is continuous as a map on pairs of states and each trajectory $u_N$ is continuous in time. Let $F$ be a candidate limiting Fourier-state trajectory. If the Galerkin forcing modes converge pointwise to the components of $F$ on every interval $[0,t]$ with $t$ nonnegative, then the data $(H,Bop)$ satisfy the dominated-convergence hypothesis for the Galerkin forcing.
background
The module ContinuumLimit2D defines the objects needed to pass from finite-dimensional 2D Galerkin approximations to a continuum Fourier-state limit while keeping every analytic step explicit. UniformBoundsHypothesis records a family of trajectories $u_N : ℕ → ℝ → GalerkinState N$ together with a single uniform norm bound $B$ that holds for all truncations and all times $t ≥ 0$. FourierState2D is the space of all sequences indexed by modes on the torus, obtained by extending truncated Galerkin states by zero outside the retained modes. GalerkinForcingDominatedConvergenceHypothesis packages the limiting trajectory $F$, an integrable dominating function, and the measurability and convergence data required to apply dominated convergence to the forcing term defined by galerkinForcing.
proof idea
The definition is a one-line wrapper around the base constructor of_convectionNormBound. It supplies the measurability field by invoking the theorem aestronglyMeasurable_galerkinForcing_mode_of_continuous under the supplied continuity hypotheses on the operators and trajectories, then passes the uniform bound, the constant $C$, the pointwise limit, and the remaining data directly to the base constructor.
why it matters in Recognition Science
This definition closes one of the analytic hypotheses required by the M5 pipeline that identifies the continuum limit of 2D Galerkin approximations. It produces an instance of GalerkinForcingDominatedConvergenceHypothesis that can be fed into later constructions of ForcingDominatedConvergenceAt. The construction follows the module's explicit policy of packaging compactness and identification steps as named hypotheses rather than hidden axioms.
scope and limits
- Does not establish the uniform bounds on the Galerkin trajectories.
- Does not prove pointwise convergence of the forcing modes to the limit trajectory.
- Does not derive the continuum Navier-Stokes equation from the Galerkin system.
- Does not address three-dimensional domains or non-periodic boundary conditions.
formal statement (Lean)
1112noncomputable def of_convectionNormBound_of_continuous
1113 (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N)
1114 (C : ℝ) (hC : 0 ≤ C)
1115 (hB : ∀ N : ℕ, ∀ u : GalerkinState N, ‖(Bop N u u)‖ ≤ C * ‖u‖ ^ 2)
1116 (hBcont : ∀ N : ℕ,
1117 Continuous (fun p : GalerkinState N × GalerkinState N => (Bop N) p.1 p.2))
1118 (hucont : ∀ N : ℕ, Continuous (H.uN N))
1119 (F : ℝ → FourierState2D)
1120 (lim : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
1121 Tendsto (fun N : ℕ => (galerkinForcing H Bop N s) k) atTop (𝓝 ((F s) k))) :
1122 GalerkinForcingDominatedConvergenceHypothesis H Bop :=
proof body
Definition body.
1123 of_convectionNormBound (H := H) (Bop := Bop) (C := C) hC (hB := hB) (F := F)
1124 (meas := by
1125 intro N t ht k
1126 exact aestronglyMeasurable_galerkinForcing_mode_of_continuous (H := H) (Bop := Bop)
1127 (hBcont := hBcont) (hucont := hucont) N t ht k)
1128 (lim := lim)
1129
1130end GalerkinForcingDominatedConvergenceHypothesis
1131
1132/-- Hypothesis: existence of a limit Fourier trajectory and convergence from the approximants. -/