Euclidean and Hermitian spaces

• Euclidean vector spaces
• Hermitian vector spaces
• Dual isomorphism in the Euclidean case
• Orthogonal complement
• Cauchy-Schwarz inequality

DefinitionNorm#

(Semi)norm constructed from a PreInnerProductSpace.Core structure, defined to be the square root of the scalar product.

InnerProductSpace.Core.toNorm.{u_1, u_3} {𝕜 : Type u_1} {F : Type u_3} [RCLike 𝕜] [AddCommGroup F]
  [_root_.Module 𝕜 F] [c : PreInnerProductSpace.Core 𝕜 F] : Norm F

Sources

• Mathlib documentation: InnerProductSpace.Core.toNorm
• Source of InnerProductSpace.Core.toNorm in Mathlib/Analysis/InnerProductSpace/Defs.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Euclidean and Hermitian spaces

MathlibInnerProductSpace.Core.toNorm

Uses 3 · Used by 1

Statement usesAssociative algebra over a commutative ring · Completeness · Metric space

Used byRiemannian manifold

TheoremOrthonormal bases#

An orthonormal set in a finite-dimensional InnerProductSpace is maximal, if and only if it is a basis.

maximal_orthonormal_iff_basis_of_finiteDimensional.{u_1, u_2} {𝕜 : Type u_1} {E : Type u_2}
  [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {v : Set E} [FiniteDimensional 𝕜 E]
  (hv : Orthonormal 𝕜 Subtype.val) :
  (∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ⇑b = Subtype.val

Sources

• Mathlib documentation: maximal_orthonormal_iff_basis_of_finiteDimensional
• Source of maximal_orthonormal_iff_basis_of_finiteDimensional in Mathlib/Analysis/InnerProductSpace/Projection/FiniteDimensional.lean
• Mathlib undergraduate list: Bilinear and Quadratic Forms Over a Vector Space › Euclidean and Hermitian spaces

Mathlibmaximal_orthonormal_iff_basis_of_finiteDimensional

Uses 7

Statement usesBasis · Finite-dimensionality · Inner product space, over \(R\) or \(C\)

Proof usesCompactness in terms of filters · Linear independence · Orthogonal complement · Range of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.