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

forcingDCTAt

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)

1008noncomputable def forcingDCTAt
1009    {H : UniformBoundsHypothesis} {Bop : (N : ℕ) → ConvectionOp N}
1010    (hF : GalerkinForcingDominatedConvergenceHypothesis H Bop)
1011    (t : ℝ) (ht : 0 ≤ t) (k : Mode2) :
1012    ForcingDominatedConvergenceAt (F_N := galerkinForcing H Bop) (F := hF.F) t k :=

proof body

Definition body.

1013  ForcingDominatedConvergenceAt.of_forall (F_N := galerkinForcing H Bop) (F := hF.F) (t := t) (k := k)
1014    (bound := hF.bound t k)
1015    (h_meas := by intro N; exact hF.meas N t ht k)
1016    (h_bound := by intro N s hs; exact hF.dom N t ht k s hs)
1017    (bound_integrable := hF.bound_integrable t ht k)
1018    (h_lim := by intro s hs; exact hF.lim t ht k s hs)
1019
1020/-- If each Galerkin trajectory `uN N` is continuous and each `Bop N` is continuous as a map
1021`(u,v) ↦ Bop N u v`, then each forcing mode `s ↦ (galerkinForcing H Bop N s) k` is continuous (hence
1022AE-strongly measurable on any finite interval). -/

used by (2)

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

depends on (20)

Lean names referenced from this declaration's body.