of_convectionNormBound
A uniform bound on Galerkin trajectories together with a quadratic norm bound on the convection operator produces an integrable dominating function for every forcing mode. Researchers constructing the 2D continuum limit from finite Galerkin systems cite this to close the domination requirement inside dominated-convergence arguments. The definition assembles the hypothesis record by setting the bound to the constant C B squared and verifies integrability by constancy on finite intervals.
claimLet $H$ be a uniform-bounds hypothesis with global bound $B$, let $Bop$ be a family of convection operators satisfying $‖Bop_N(u,u)‖ ≤ C ‖u‖² for $C ≥ 0$, and let $F : ℝ → FourierState2D$. Suppose the Galerkin forcing modes are strongly measurable on each interval $[0,t]$ and converge pointwise to $F(s)$. Then the structure GalerkinForcingDominatedConvergenceHypothesis $H$ $Bop$ holds with dominating bound equal to the constant $C B²$.
background
The ContinuumLimit2D module packages the analytic steps needed to pass from finite-dimensional 2D Galerkin approximations of incompressible flow to a continuum Fourier coefficient state. FourierState2D is the type Mode2 → VelCoeff representing the full infinite-dimensional velocity field on the torus. The Galerkin forcing is defined by galerkinForcing H Bop := extendByZero ∘ (Bop N (H.uN N s) (H.uN N s)).
proof idea
The definition uses classical refinement to build the hypothesis record. It supplies the supplied limiting field F, sets the dominating bound to the constant function C · H.B², and obtains bound_integrable by simplification because a constant is interval-integrable on any finite interval. The dom field is discharged by applying the uniform trajectory bound to obtain ‖uN N s‖ ≤ B, squaring the inequality, invoking the assumed convection bound hB, and finally applying norm_extendByZero_le to transfer the norm control to each Fourier coefficient.
why it matters in Recognition Science
This supplies a concrete, checkable route to the dominated-convergence hypothesis for the Galerkin forcing inside the 2D continuum-limit pipeline. It is invoked directly by the downstream definition of_convectionNormBound_of_continuous, which further discharges measurability once continuity of Bop is assumed. In the Recognition Science monolith the construction closes one explicit analytic-compactness requirement of milestone M5, keeping the dependency graph free of axioms or hidden hypotheses.
scope and limits
- Does not derive the uniform trajectory bound B from energy or enstrophy estimates.
- Does not establish pointwise convergence of the forcing modes to F.
- Does not treat three-dimensional or compressible flows.
- Does not supply convergence rates or explicit constants beyond C and B.
formal statement (Lean)
1055noncomputable def of_convectionNormBound
1056 (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N)
1057 (C : ℝ) (hC : 0 ≤ C)
1058 (hB : ∀ N : ℕ, ∀ u : GalerkinState N, ‖(Bop N u u)‖ ≤ C * ‖u‖ ^ 2)
1059 (F : ℝ → FourierState2D)
1060 (meas : ∀ N : ℕ, ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
1061 MeasureTheory.AEStronglyMeasurable
1062 (fun s : ℝ => (galerkinForcing H Bop N s) k)
1063 (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t)))
1064 (lim : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
1065 Tendsto (fun N : ℕ => (galerkinForcing H Bop N s) k) atTop (𝓝 ((F s) k))) :
1066 GalerkinForcingDominatedConvergenceHypothesis H Bop :=
proof body
Definition body.
1067by
1068 classical
1069 refine
1070 { F := F
1071 bound := fun _t _k _s => C * H.B ^ 2
1072 bound_integrable := by
1073 intro t _ht k
1074 -- constant function is interval integrable on any finite interval
1075 simp
1076 meas := meas
1077 dom := ?_
1078 lim := lim }
1079 intro N t ht k s hs
1080 -- from `s ∈ uIoc 0 t` and `0 ≤ t`, we have `0 < s` hence `0 ≤ s`.
1081 have hs' : 0 < s ∧ s ≤ t := by
1082 have hs'' : min (0 : ℝ) t < s ∧ s ≤ max (0 : ℝ) t := by
1083 simpa [Set.uIoc, Set.mem_Ioc] using hs
1084 simpa [min_eq_left ht, max_eq_right ht] using hs''
1085 have hs0 : 0 ≤ s := le_of_lt hs'.1
1086
1087 -- uniform bound on `uN`
1088 have hu : ‖H.uN N s‖ ≤ H.B := H.bound N s hs0
1089
1090 -- square the bound: `‖u‖^2 ≤ B^2`
1091 have hu_sq : ‖H.uN N s‖ ^ 2 ≤ H.B ^ 2 := by
1092 have : ‖H.uN N s‖ * ‖H.uN N s‖ ≤ H.B * H.B :=
1093 mul_le_mul hu hu (norm_nonneg _) H.B_nonneg
1094 simpa [pow_two] using this
1095
1096 -- control the Galerkin nonlinearity in norm, then pass to a single Fourier coefficient
1097 have hBuu : ‖(Bop N (H.uN N s) (H.uN N s))‖ ≤ C * ‖H.uN N s‖ ^ 2 :=
1098 hB N (H.uN N s)
1099 have hBuu' : ‖(Bop N (H.uN N s) (H.uN N s))‖ ≤ C * H.B ^ 2 :=
1100 le_trans hBuu (mul_le_mul_of_nonneg_left hu_sq hC)
1101 have hcoeff :
1102 ‖(galerkinForcing H Bop N s) k‖ ≤ C * H.B ^ 2 := by
1103 have h1 :
1104 ‖(galerkinForcing H Bop N s) k‖ ≤ ‖(Bop N (H.uN N s) (H.uN N s))‖ := by
1105 simpa [galerkinForcing] using
1106 (norm_extendByZero_le (u := (Bop N (H.uN N s) (H.uN N s))) (k := k))
1107 exact le_trans h1 hBuu'
1108 simpa using hcoeff
1109
1110/-- Combine `of_convectionNormBound` with continuity assumptions to discharge measurability of the
1111Galerkin forcing modes automatically. -/