Orthonormal sets

This file defines orthonormal sets in inner product spaces.

Main results

• We define Orthonormal, a predicate on a function v : ι → E, and prove the existence of a maximal orthonormal set, exists_maximal_orthonormal.
• Bessel's inequality, Orthonormal.tsum_inner_products_le, states that given an orthonormal set v and a vector x, the sum of the norm-squares of the inner products ⟪v i, x⟫ is no more than the norm-square of x.

For the existence of orthonormal bases, Hilbert bases, etc., see the file Analysis.InnerProductSpace.projection.

def Orthonormal (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (v : ι → E) : Prop

An orthonormal set of vectors in an InnerProductSpace

Equations

• Orthonormal 𝕜 v = ((∀ (i : ι), ‖v i‖ = 1) ∧ Pairwise fun (i j : ι) => inner 𝕜 (v i) (v j) = 0)

@[simp]

theorem Orthonormal.of_isEmpty {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [IsEmpty ι] (v : ι → E) : Orthonormal 𝕜 v

@[simp]

theorem orthonormal_vecCons_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {n : ℕ} {v : E} {vs : Fin n → E} : Orthonormal 𝕜 (Matrix.vecCons v vs) ↔ ‖v‖ = 1 ∧ (∀ (i : Fin n), inner 𝕜 v (vs i) = 0) ∧ Orthonormal 𝕜 vs

theorem Orthonormal.norm_eq_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (h : Orthonormal 𝕜 v) (i : ι) : ‖v i‖ = 1

theorem Orthonormal.nnNorm_eq_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (h : Orthonormal 𝕜 v) (i : ι) : ‖v i‖₊ = 1

@[deprecated Orthonormal.nnNorm_eq_one (since := "2026-10-31")]

theorem Orthonormal.nnnorm_eq_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (h : Orthonormal 𝕜 v) (i : ι) : ‖v i‖₊ = 1

Alias of Orthonormal.nnNorm_eq_one.

theorem Orthonormal.enorm_eq_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (h : Orthonormal 𝕜 v) (i : ι) : ‖v i‖ₑ = 1

theorem Orthonormal.inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} {i j : ι} (h : Orthonormal 𝕜 v) (hij : i ≠ j) : inner 𝕜 (v i) (v j) = 0

theorem orthonormal_iff_ite {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [DecidableEq ι] {v : ι → E} : Orthonormal 𝕜 v ↔ ∀ (i j : ι), inner 𝕜 (v i) (v j) = if i = j then 1 else 0

if ... then ... else characterization of an indexed set of vectors being orthonormal. (Inner product equals Kronecker delta.)

@[simp]

theorem orthonormal_subsingleton_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Subsingleton ι] {v : ι → E} : Orthonormal 𝕜 v ↔ ∀ (i : ι), ‖v i‖ = 1

theorem orthonormal_subtype_iff_ite {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] [DecidableEq E] {s : Set E} : Orthonormal 𝕜 Subtype.val ↔ ∀ v ∈ s, ∀ w ∈ s, inner 𝕜 v w = if v = w then 1 else 0

if ... then ... else characterization of a set of vectors being orthonormal. (Inner product equals Kronecker delta.)

theorem Orthonormal.inner_right_finsupp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) : inner 𝕜 (v i) ((Finsupp.linearCombination 𝕜 v) l) = l i

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

theorem Orthonormal.inner_right_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι} {i : ι} (hi : i ∈ s) : inner 𝕜 (v i) (∑ i ∈ s, l i • v i) = l i

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

theorem Orthonormal.inner_right_fintype {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) : inner 𝕜 (v i) (∑ i : ι, l i • v i) = l i

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

theorem Orthonormal.inner_left_finsupp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι →₀ 𝕜) (i : ι) : inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l) (v i) = (starRingEnd 𝕜) (l i)

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

theorem Orthonormal.inner_left_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) {s : Finset ι} {i : ι} (hi : i ∈ s) : inner 𝕜 (∑ i ∈ s, l i • v i) (v i) = (starRingEnd 𝕜) (l i)

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

theorem Orthonormal.inner_left_fintype {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (l : ι → 𝕜) (i : ι) : inner 𝕜 (∑ i : ι, l i • v i) (v i) = (starRingEnd 𝕜) (l i)

The inner product of a linear combination of a set of orthonormal vectors with one of those vectors picks out the coefficient of that vector.

theorem Orthonormal.inner_finsupp_eq_sum_left {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) : inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l₁) ((Finsupp.linearCombination 𝕜 v) l₂) = l₁.sum fun (i : ι) (y : 𝕜) => (starRingEnd 𝕜) y * l₂ i

The inner product of two linear combinations of a set of orthonormal vectors, expressed as a sum over the first Finsupp.

theorem Orthonormal.inner_finsupp_eq_sum_right {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι →₀ 𝕜) : inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l₁) ((Finsupp.linearCombination 𝕜 v) l₂) = l₂.sum fun (i : ι) (y : 𝕜) => (starRingEnd 𝕜) (l₁ i) * y

The inner product of two linear combinations of a set of orthonormal vectors, expressed as a sum over the second Finsupp.

theorem Orthonormal.inner_sum {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (l₁ l₂ : ι → 𝕜) (s : Finset ι) : inner 𝕜 (∑ i ∈ s, l₁ i • v i) (∑ i ∈ s, l₂ i • v i) = ∑ i ∈ s, (starRingEnd 𝕜) (l₁ i) * l₂ i

The inner product of two linear combinations of a set of orthonormal vectors, expressed as a sum.

theorem Orthonormal.inner_left_right_finset {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {s : Finset ι} {v : ι → E} (hv : Orthonormal 𝕜 v) {a : ι → ι → 𝕜} : ∑ i ∈ s, ∑ j ∈ s, a i j • inner 𝕜 (v j) (v i) = ∑ k ∈ s, a k k

The double sum of weighted inner products of pairs of vectors from an orthonormal sequence is the sum of the weights.

theorem Orthonormal.linearIndependent {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : LinearIndependent 𝕜 v

An orthonormal set is linearly independent.

theorem Orthonormal.comp {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {v : ι → E} (hv : Orthonormal 𝕜 v) (f : ι' → ι) (hf : Function.Injective f) : Orthonormal 𝕜 (v ∘ f)

A subfamily of an orthonormal family (i.e., a composition with an injective map) is an orthonormal family.

theorem orthonormal_subtype_range {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Function.Injective v) : Orthonormal 𝕜 Subtype.val ↔ Orthonormal 𝕜 v

An injective family v : ι → E is orthonormal if and only if Subtype.val : (range v) → E is orthonormal.

theorem Orthonormal.toSubtypeRange {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) : Orthonormal 𝕜 Subtype.val

If v : ι → E is an orthonormal family, then Subtype.val : (range v) → E is an orthonormal family.

theorem Orthonormal.inner_finsupp_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) {s : Set ι} {i : ι} (hi : i ∉ s) {l : ι →₀ 𝕜} (hl : l ∈ Finsupp.supported 𝕜 𝕜 s) : inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l) (v i) = 0

A linear combination of some subset of an orthonormal set is orthogonal to other members of the set.

theorem Orthonormal.orthonormal_of_forall_eq_or_eq_neg {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v w : ι → E} (hv : Orthonormal 𝕜 v) (hw : ∀ (i : ι), w i = v i ∨ w i = -v i) : Orthonormal 𝕜 w

Given an orthonormal family, a second family of vectors is orthonormal if every vector equals the corresponding vector in the original family or its negation.

theorem orthonormal_empty (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Orthonormal 𝕜 fun (x : ↑∅) => ↑x

theorem orthonormal_iUnion_of_directed {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {η : Type u_5} {s : η → Set E} (hs : Directed (fun (x1 x2 : Set E) => x1 ⊆ x2) s) (h : ∀ (i : η), Orthonormal 𝕜 fun (x : ↑(s i)) => ↑x) : Orthonormal 𝕜 fun (x : ↑(⋃ (i : η), s i)) => ↑x

theorem orthonormal_sUnion_of_directed {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set (Set E)} (hs : DirectedOn (fun (x1 x2 : Set E) => x1 ⊆ x2) s) (h : ∀ a ∈ s, Orthonormal 𝕜 fun (x : ↑a) => ↑x) : Orthonormal 𝕜 fun (x : ↑(⋃₀ s)) => ↑x

theorem exists_maximal_orthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {s : Set E} (hs : Orthonormal 𝕜 Subtype.val) : ∃ w ⊇ s, Orthonormal 𝕜 Subtype.val ∧ ∀ u ⊇ w, Orthonormal 𝕜 Subtype.val → u = w

Given an orthonormal set v of vectors in E, there exists a maximal orthonormal set containing it.

noncomputable def basisOfOrthonormalOfCardEqFinrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [Nonempty ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (card_eq : Fintype.card ι = Module.finrank 𝕜 E) : Module.Basis ι 𝕜 E

A family of orthonormal vectors with the correct cardinality forms a basis.

Equations

• basisOfOrthonormalOfCardEqFinrank hv card_eq = basisOfLinearIndependentOfCardEqFinrank ⋯ card_eq

@[simp]

theorem coe_basisOfOrthonormalOfCardEqFinrank {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} [Fintype ι] [Nonempty ι] {v : ι → E} (hv : Orthonormal 𝕜 v) (card_eq : Fintype.card ι = Module.finrank 𝕜 E) : ⇑(basisOfOrthonormalOfCardEqFinrank hv card_eq) = v

theorem Orthonormal.ne_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : ι → E} (hv : Orthonormal 𝕜 v) (i : ι) : v i ≠ 0

theorem LinearIsometry.orthonormal_comp_iff {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : ι → E} (f : E →ₗᵢ[𝕜] E') : Orthonormal 𝕜 (⇑f ∘ v) ↔ Orthonormal 𝕜 v

A linear isometry preserves the property of being orthonormal.

theorem Orthonormal.comp_linearIsometry {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : ι → E} (hv : Orthonormal 𝕜 v) (f : E →ₗᵢ[𝕜] E') : Orthonormal 𝕜 (⇑f ∘ v)

A linear isometry preserves the property of being orthonormal.

theorem Orthonormal.comp_linearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : ι → E} (hv : Orthonormal 𝕜 v) (f : E ≃ₗᵢ[𝕜] E') : Orthonormal 𝕜 (⇑f ∘ v)

A linear isometric equivalence preserves the property of being orthonormal.

theorem Orthonormal.mapLinearIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (f : E ≃ₗᵢ[𝕜] E') : Orthonormal 𝕜 ⇑(v.map f.toLinearEquiv)

A linear isometric equivalence, applied with Basis.map, preserves the property of being orthonormal.

def LinearMap.isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : E →ₗᵢ[𝕜] E'

A linear map that sends an orthonormal basis to orthonormal vectors is a linear isometry.

Equations

• f.isometryOfOrthonormal hv hf = f.isometryOfInner ⋯

@[simp]

theorem LinearMap.coe_isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : ⇑(f.isometryOfOrthonormal hv hf) = ⇑f

@[simp]

theorem LinearMap.isometryOfOrthonormal_toLinearMap {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E →ₗ[𝕜] E') {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : (f.isometryOfOrthonormal hv hf).toLinearMap = f

def LinearEquiv.isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : E ≃ₗᵢ[𝕜] E'

A linear equivalence that sends an orthonormal basis to orthonormal vectors is a linear isometric equivalence.

Equations

• f.isometryOfOrthonormal hv hf = f.isometryOfInner ⋯

@[simp]

theorem LinearEquiv.coe_isometryOfOrthonormal {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : ⇑(f.isometryOfOrthonormal hv hf) = ⇑f

@[simp]

theorem LinearEquiv.isometryOfOrthonormal_toLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] (f : E ≃ₗ[𝕜] E') {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) (hf : Orthonormal 𝕜 (⇑f ∘ ⇑v)) : (f.isometryOfOrthonormal hv hf).toLinearEquiv = f

noncomputable def Orthonormal.equiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : E ≃ₗᵢ[𝕜] E'

A linear isometric equivalence that sends an orthonormal basis to a given orthonormal basis.

Equations

• hv.equiv hv' e = (v.equiv v' e).isometryOfOrthonormal hv ⋯

@[simp]

theorem Orthonormal.equiv_toLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : (hv.equiv hv' e).toLinearEquiv = v.equiv v' e

@[simp]

theorem Orthonormal.equiv_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {ι' : Type u_9} {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') (i : ι) : (hv.equiv hv' e) (v i) = v' (e i)

@[simp]

theorem Orthonormal.equiv_trans {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {ι'' : Type u_6} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {E'' : Type u_8} [SeminormedAddCommGroup E''] [InnerProductSpace 𝕜 E''] {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') {v'' : Module.Basis ι'' 𝕜 E''} (hv'' : Orthonormal 𝕜 ⇑v'') (e' : ι' ≃ ι'') : (hv.equiv hv' e).trans (hv'.equiv hv'' e') = hv.equiv hv'' (e.trans e')

theorem Orthonormal.map_equiv {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_7} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : v.map (hv.equiv hv' e).toLinearEquiv = v'.reindex e.symm

@[simp]

theorem Orthonormal.equiv_refl {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) : hv.equiv hv (Equiv.refl ι) = LinearIsometryEquiv.refl 𝕜 E

@[simp]

theorem Orthonormal.equiv_symm {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} {ι' : Type u_5} {E' : Type u_6} [SeminormedAddCommGroup E'] [InnerProductSpace 𝕜 E'] {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι') : (hv.equiv hv' e).symm = hv'.equiv hv e.symm

theorem Orthonormal.sum_inner_products_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E} {s : Finset ι} (hv : Orthonormal 𝕜 v) : ∑ i ∈ s, ‖inner 𝕜 (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality for finite sums.

theorem Orthonormal.tsum_inner_products_le {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E} (hv : Orthonormal 𝕜 v) : ∑' (i : ι), ‖inner 𝕜 (v i) x‖ ^ 2 ≤ ‖x‖ ^ 2

Bessel's inequality.

theorem Orthonormal.inner_products_summable {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {ι : Type u_4} (x : E) {v : ι → E} (hv : Orthonormal 𝕜 v) : Summable fun (i : ι) => ‖inner 𝕜 (v i) x‖ ^ 2

The sum defined in Bessel's inequality is summable.