Hilbert bases #
This file transfers orthogonality to every vector of a subspace from orthogonality to each element of a Hilbert basis of that subspace. In particular, this lets Hilbert bases of mutually orthogonal eigenspaces be assembled into a spectral basis of the ambient space.
theorem
HilbertBasis.inner_eq_zero_of_forall_inner_eq_zero
{𝕜 : Type u_1}
{E : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup E]
[InnerProductSpace 𝕜 E]
{K : Submodule 𝕜 E}
{iota : Type u_3}
(bK : HilbertBasis iota 𝕜 ↥K)
{x : E}
(hx : ∀ (i : iota), inner 𝕜 x ↑(bK i) = 0)
{y : E}
(hy : y ∈ K)
:
A vector orthogonal to every member of a Hilbert basis of a subspace is orthogonal to every vector of the represented subspace.