The Lean 4 theorem `galerkinProj_tendsto` in the `ChapterHermiteGalerkinFriedrichs` chapter of the timepiece formalization
ProvedBookProof.HermiteGalerkin.galerkinProj_tendstotimepiece
The Lean 4 theorem galerkinProj_tendsto in the ChapterHermiteGalerkinFriedrichs chapter of the timepiece formalization.
Preamble
-- Generated from ChapterHermiteGalerkinFriedrichs.lean — theorem BookProof.HermiteGalerkin.galerkinProj_tendsto
import Mathlib
import Definitions.Def_ChapterHermiteGalerkinFriedrichs
open BookProof.HermiteGalerkin
open BookProof.FarisLavine BookProof.YangMillsFriedrichs BookProof.YangMillsFriedrichsLimit
open Filter Topology
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]
variable {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℂ F]Formal statement
theorem BookProof.HermiteGalerkin.galerkinProj_tendsto (b : HilbertBasis ℕ ℂ F) (u : F) :
Tendsto (fun m : ℕ => (galerkinSpan b m).starProjection u) atTop (nhds u) := by sorrySource