(b : HilbertBasis ℕ ℂ F) (S : Submodule ℂ F) [FiniteDimensional ℂ S] {ε : ℝ} (hε : 0 < ε) : ∃ m₀ : ℕ, ∀ m ≥ m₀, ∀ x ∈ S, ‖(galerkinSpan b m).starProjection x

Initializing...

(b : HilbertBasis ℕ ℂ F) (S : Submodule ℂ F) [FiniteDimensional ℂ S] {ε : ℝ} (hε : 0 < ε) : ∃ m₀ : ℕ, ∀ m ≥ m₀, ∀ x ∈ S, ‖(galerkinSpan b m).starProjection x - x‖ ≤ ε * ‖x‖ · Prove2Me