of_convectionNormBound_of_continuous

formal source

1109
1110/-- Combine `of_convectionNormBound` with continuity assumptions to discharge measurability of the
1111Galerkin forcing modes automatically. -/
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 :=
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. -/
1133structure ConvergenceHypothesis (H : UniformBoundsHypothesis) where
1134  /-- Candidate limit (time → full Fourier coefficients). -/
1135  u : ℝ → FourierState2D
1136  /-- Pointwise (mode-by-mode) convergence of the zero-extended Galerkin coefficients. -/
1137  converges : ∀ t : ℝ, ∀ k : Mode2,
1138    Tendsto (fun N : ℕ => (extendByZero (H.uN N t)) k) atTop (𝓝 ((u t) k))
1139
1140namespace ConvergenceHypothesis
1141
1142/-- Derived fact: if the approximants are uniformly bounded in the Galerkin norm for `t ≥ 0`,