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

galerkinForcing

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)

 971noncomputable def galerkinForcing (H : UniformBoundsHypothesis) (Bop : (N : ℕ) → ConvectionOp N) :
 972    ℕ → ℝ → FourierState2D :=

proof body

Definition body.

 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. -/

used by (7)

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

depends on (19)

Lean names referenced from this declaration's body.