def OrthonormalBases.IsOrthonormalSequence (𝕜 : Type u_3) [RCLike 𝕜] {E : Type u_4} [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (φ : ℕ → E) : Prop

theorem OrthonormalBases.IsOrthonormalSequence.norm_eq_one {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {φ : ℕ → E} (h : IsOrthonormalSequence 𝕜 φ) (n : ℕ) : ‖φ n‖ = 1

theorem OrthonormalBases.IsOrthonormalSequence.inner_eq_zero {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {φ : ℕ → E} (h : IsOrthonormalSequence 𝕜 φ) {n m : ℕ} (hne : n ≠ m) : inner 𝕜 (φ n) (φ m) = 0

theorem OrthonormalBases.inner_tendsto_of_tendsto {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_3} {l : Filter α} {u v : α → E} {a b : E} (hu : Filter.Tendsto u l (nhds a)) (hv : Filter.Tendsto v l (nhds b)) : Filter.Tendsto (fun (n : α) => inner 𝕜 (u n) (v n)) l (nhds (inner 𝕜 a b))

theorem OrthonormalBases.hasSum_inner_smul_of_dense_span {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {φ : ℕ → E} (hφ : Orthonormal 𝕜 φ) (ha : (Submodule.span 𝕜 (Set.range φ)).topologicalClosure = ⊤) (f : E) : HasSum (fun (n : ℕ) => inner 𝕜 (φ n) f • φ n) f

theorem OrthonormalBases.parseval_of_dense_span {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {φ : ℕ → E} (hφ : Orthonormal 𝕜 φ) (ha : (Submodule.span 𝕜 (Set.range φ)).topologicalClosure = ⊤) (f : E) : HasSum (fun (n : ℕ) => ‖inner 𝕜 (φ n) f‖ ^ 2) (‖f‖ ^ 2)

theorem OrthonormalBases.dense_span_of_hasSum_inner_smul {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {φ : ℕ → E} (hc : ∀ (f : E), HasSum (fun (n : ℕ) => inner 𝕜 (φ n) f • φ n) f) : (Submodule.span 𝕜 (Set.range φ)).topologicalClosure = ⊤

theorem OrthonormalBases.dense_span_of_parseval {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {φ : ℕ → E} (hb : ∀ (f : E), HasSum (fun (n : ℕ) => ‖inner 𝕜 (φ n) f‖ ^ 2) (‖f‖ ^ 2)) : (Submodule.span 𝕜 (Set.range φ)).topologicalClosure = ⊤

theorem OrthonormalBases.inner_hasSum_of_orthonormal_series {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {φ : ℕ → E} (hφ : Orthonormal 𝕜 φ) {a b : ℕ → 𝕜} {u v : E} (hu : HasSum (fun (n : ℕ) => a n • φ n) u) (hv : HasSum (fun (n : ℕ) => b n • φ n) v) : HasSum (fun (n : ℕ) => (starRingEnd 𝕜) (a n) * b n) (inner 𝕜 u v)

class HilbertSpace.IsHilbertSpace (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] : Prop