pith. machine review for the scientific record. sign in
structure definition def or abbrev

GalerkinForcingDominatedConvergenceHypothesis

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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 →
1002    Tendsto (fun N : ℕ => (galerkinForcing H Bop N s) k) atTop (𝓝 ((F s) k))
1003
1004namespace GalerkinForcingDominatedConvergenceHypothesis
1005
1006/-- Build `ForcingDominatedConvergenceAt` for the Galerkin forcing from the more concrete hypothesis
1007`GalerkinForcingDominatedConvergenceHypothesis`. -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (22)

Lean names referenced from this declaration's body.