Finite-dimensional inner product spaces (see also Hilbert spaces, below)

StructureExistence of orthonormal basis#

An orthonormal basis on E is an identification of E with its dimensional-matching EuclideanSpace 𝕜 ι.

OrthonormalBasis.{u_1, u_3, u_4} (ι : Type u_1) (𝕜 : Type u_3) [RCLike 𝕜] (E : Type u_4)
  [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [Fintype ι] : Type (max (max u_1 u_3) u_4)

Sources

• Mathlib documentation: OrthonormalBasis
• Source of OrthonormalBasis in Mathlib/Analysis/InnerProductSpace/PiL2.lean
• Mathlib overview: Linear algebra › Finite-dimensional inner product spaces (see also Hilbert spaces, below)

MathlibOrthonormalBasis

Uses 3 · Used by 3

Statement usesFinite set · Inner product space, over \(R\) or \(C\) · Linear map

Used bySphere · Diagonalization of self-adjoint endomorphisms · Inscribed angle theorem

TheoremDiagonalization of self-adjoint endomorphisms#

Diagonalization theorem, spectral theorem; version 2: A self-adjoint operator T on a finite-dimensional inner product space E acts diagonally on the identification of E with Euclidean space induced by an orthonormal basis of eigenvectors of T.

LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜]
  {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →ₗ[𝕜] E}
  [FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) (v : E)
  (i : Fin n) :
  ((hT.eigenvectorBasis hn).repr (T v)).ofLp i =
    ↑(hT.eigenvalues hn i) * ((hT.eigenvectorBasis hn).repr v).ofLp i

Sources

• Mathlib documentation: LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply
• Source of LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply in Mathlib/Analysis/InnerProductSpace/Spectrum.lean
• Mathlib overview: Linear algebra › Finite-dimensional inner product spaces (see also Hilbert spaces, below)
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Endomorphisms

MathlibLinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply

Uses 12

Statement usesCardinal · Direct sum · Existence of orthonormal basis · Finite-dimensionality · Generalized eigenspaces · Isomorphism with \(K^n\) · Linear independence · Range of a linear map

Proof usesEigenvalue · Eigenvalues from Rayleigh quotient · Local ring · Orthogonal complement

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.