galerkinForcing

formal source

 968/-- The (Galerkin) nonlinear forcing family in full Fourier variables:
 969
 970`F_N(N,s) := extendByZero (Bop N (uN N s) (uN N s))`. -/
 971noncomputable def galerkinForcing (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N) :
 972    ℕ → ℝ → FourierState2D :=
 973  fun N s => extendByZero ((Bop N) (H.uN N s) (H.uN N s))
 974
 975/-- A more concrete, user-facing hypothesis for dominated convergence of the *Galerkin forcing*
 976`galerkinForcing H Bop`, expressed directly in terms of:
 977
 978- measurability of the forcing modes,
 979- an integrable dominating function on each time interval `[0,t]`, and
 980- pointwise convergence of forcing modes.
 981
 982This packages exactly what you need to build `ForcingDominatedConvergenceAt` for the Galerkin forcing. -/
 983structure GalerkinForcingDominatedConvergenceHypothesis
 984    (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N) where
 985  /-- Limiting forcing in full Fourier variables. -/
 986  F : ℝ → FourierState2D
 987  /-- Dominating `L¹` bound, allowed to depend on `(t,k)`. -/
 988  bound : ℝ → Mode2 → ℝ → ℝ
 989  /-- Integrability of the dominating bound on each interval `0..t` (for `t ≥ 0`). -/
 990  bound_integrable : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
 991    IntervalIntegrable (bound t k) MeasureTheory.volume (0 : ℝ) t
 992  /-- Strong measurability (in `s`) of each forcing mode on `0..t` (for `t ≥ 0`). -/
 993  meas : ∀ N : ℕ, ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2,
 994    MeasureTheory.AEStronglyMeasurable
 995      (fun s : ℝ => (galerkinForcing H Bop N s) k)
 996      (MeasureTheory.volume.restrict (Set.uIoc (0 : ℝ) t))
 997  /-- Pointwise domination by the integrable bound on `0..t` (for `t ≥ 0`). -/
 998  dom : ∀ N : ℕ, ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →
 999    ‖(galerkinForcing H Bop N s) k‖ ≤ bound t k s
1000  /-- Pointwise convergence of forcing modes on `0..t` (for `t ≥ 0`). -/
1001  lim : ∀ t : ℝ, t ≥ 0 → ∀ k : Mode2, ∀ s : ℝ, s ∈ Set.uIoc (0 : ℝ) t →