# 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`.

source
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)

Instances For

source
@[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
source
@[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
source
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
source
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
source
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
source
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
source
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.)

source
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.)

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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`.

source
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`.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
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.

source
theorem orthonormal_empty (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] :
Orthonormal 𝕜 fun (x : ↑∅) => ↑x
source
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
source
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
source
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.

source
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

Instances For

source
@[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
source
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
source
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.

source
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.

source
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.

source
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.

source
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 ⋯

Instances For

source
@[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
source
@[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
source
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 ⋯

Instances For

source
@[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
source
@[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
source
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 ⋯

Instances For

source
@[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
source
@[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)
source
@[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')
source
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
source
@[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
source
@[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
source
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.

source
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.

source
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.