mathlib3documentation

analysis.inner_product_space.pi_L2

L² inner product space structure on finite products of inner product spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The L² norm on a finite product of inner product spaces is compatible with an inner product $$\langle x, y\rangle = \sum \langle x_i, y_i \rangle.$$ This is recorded in this file as an inner product space instance on pi_Lp 2.

This file develops the notion of a finite dimensional Hilbert space over 𝕜 = ℂ, ℝ, referred to as E. We define an orthonormal_basis 𝕜 ι E as a linear isometric equivalence between E and euclidean_space 𝕜 ι. Then std_orthonormal_basis shows that such an equivalence always exists if E is finite dimensional. We provide language for converting between a basis that is orthonormal and an orthonormal basis (e.g. basis.to_orthonormal_basis). We show that orthonormal bases for each summand in a direct sum of spaces can be combined into an orthonormal basis for the the whole sum in direct_sum.submodule_is_internal.subordinate_orthonormal_basis. In the last section, various properties of matrices are explored.

Main definitions #

• euclidean_space 𝕜 n: defined to be pi_Lp 2 (n → 𝕜) for any fintype n, i.e., the space from functions to n to 𝕜 with the L² norm. We register several instances on it (notably that it is a finite-dimensional inner product space).

• orthonormal_basis 𝕜 ι: defined to be an isometry to Euclidean space from a given finite-dimensional innner product space, E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι.

• basis.to_orthonormal_basis: constructs an orthonormal_basis for a finite-dimensional Euclidean space from a basis which is orthonormal.

• orthonormal.exists_orthonormal_basis_extension: provides an existential result of an orthonormal_basis extending a given orthonormal set

• exists_orthonormal_basis: provides an orthonormal basis on a finite dimensional vector space

• std_orthonormal_basis: provides an arbitrarily-chosen orthonormal_basis of a given finite dimensional inner product space

For consequences in infinite dimension (Hilbert bases, etc.), see the file analysis.inner_product_space.l2_space.

@[protected, instance]
noncomputable def pi_Lp.inner_product_space {𝕜 : Type u_3} [is_R_or_C 𝕜] {ι : Type u_1} [fintype ι] (f : ι Type u_2) [Π (i : ι), ] [Π (i : ι), (f i)] :
(pi_Lp 2 f)
Equations
@[simp]
theorem pi_Lp.inner_apply {𝕜 : Type u_3} [is_R_or_C 𝕜] {ι : Type u_1} [fintype ι] {f : ι Type u_2} [Π (i : ι), ] [Π (i : ι), (f i)] (x y : f) :
= finset.univ.sum (λ (i : ι), has_inner.inner (x i) (y i))
@[nolint, reducible]
def euclidean_space (𝕜 : Type u_1) [is_R_or_C 𝕜] (n : Type u_2) [fintype n] :
Type (max u_2 u_1)

The standard real/complex Euclidean space, functions on a finite type. For an n-dimensional space use euclidean_space 𝕜 (fin n).

Equations
• = (λ (i : n), 𝕜)
theorem euclidean_space.nnnorm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x : n) :
theorem euclidean_space.norm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x : n) :
x = (finset.univ.sum (λ (i : n), x i ^ 2))
theorem euclidean_space.dist_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x y : n) :
= (finset.univ.sum (λ (i : n), has_dist.dist (x i) (y i) ^ 2))
theorem euclidean_space.nndist_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x y : n) :
= nnreal.sqrt (finset.univ.sum (λ (i : n), has_nndist.nndist (x i) (y i) ^ 2))
theorem euclidean_space.edist_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x y : n) :
= finset.univ.sum (λ (i : n), has_edist.edist (x i) (y i) ^ 2) ^ (1 / 2)
@[protected, instance]
def euclidean_space.finite_dimensional {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] :
@[protected, instance]
noncomputable def euclidean_space.inner_product_space {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] :
Equations
@[simp]
theorem finrank_euclidean_space {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] :
theorem finrank_euclidean_space_fin {𝕜 : Type u_3} [is_R_or_C 𝕜] {n : } :
(fin n)) = n
theorem euclidean_space.inner_eq_star_dot_product {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (x y : ι) :
= matrix.dot_product (has_star.star ( (λ (i : ι), 𝕜)) x)) ( (λ (i : ι), 𝕜)) y)
theorem euclidean_space.inner_pi_Lp_equiv_symm {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (x y : ι 𝕜) :
has_inner.inner (((pi_Lp.equiv 2 (λ (ᾰ : ι), 𝕜)).symm) x) (((pi_Lp.equiv 2 (λ (ᾰ : ι), 𝕜)).symm) y) =
noncomputable def direct_sum.is_internal.isometry_L2_of_orthogonal_family {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [decidable_eq ι] {V : ι E} (hV : direct_sum.is_internal V) (hV' : (λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :
E ≃ₗᵢ[𝕜] (λ (i : ι), (V i))

A finite, mutually orthogonal family of subspaces of E, which span E, induce an isometry from E to pi_Lp 2 of the subspaces equipped with the L2 inner product.

Equations
@[simp]
theorem direct_sum.is_internal.isometry_L2_of_orthogonal_family_symm_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [decidable_eq ι] {V : ι E} (hV : direct_sum.is_internal V) (hV' : (λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)) (w : (λ (i : ι), (V i))) :
((hV.isometry_L2_of_orthogonal_family hV').symm) w = finset.univ.sum (λ (i : ι), (w i))
noncomputable def euclidean_space.equiv (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] :
≃L[𝕜] ι 𝕜

pi_Lp.linear_equiv upgraded to a continuous linear map between euclidean_space 𝕜 ι and ι → 𝕜.

Equations
@[simp]
theorem euclidean_space.equiv_to_linear_equiv_apply (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] (ᾰ : (λ (i : ι), 𝕜)) (i : ι) :
i = ᾰ i
@[simp]
theorem euclidean_space.equiv_apply (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] (ᾰ : (λ (i : ι), 𝕜)) (i : ι) :
i = ᾰ i
@[simp]
theorem euclidean_space.equiv_symm_apply (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] (ᾰ : Π (i : ι), (λ (i : ι), 𝕜) i) :
𝕜).symm) = ((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm)
@[simp]
theorem euclidean_space.equiv_to_linear_equiv_symm_apply (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] (ᾰ : Π (i : ι), (λ (i : ι), 𝕜) i) :
= ((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm)
noncomputable def euclidean_space.projₗ {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) :
→ₗ[𝕜] 𝕜

The projection on the i-th coordinate of euclidean_space 𝕜 ι, as a linear map.

Equations
@[simp]
theorem euclidean_space.projₗ_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) (ᾰ : ι) :
= ᾰ i
@[simp]
theorem euclidean_space.proj_coe {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) :
@[simp]
theorem euclidean_space.proj_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) (ᾰ : ι) :
= ᾰ i
noncomputable def euclidean_space.proj {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) :
→L[𝕜] 𝕜

The projection on the i-th coordinate of euclidean_space 𝕜 ι, as a continuous linear map.

Equations
noncomputable def euclidean_space.single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :

The vector given in euclidean space by being 1 : 𝕜 at coordinate i : ι and 0 : 𝕜 at all other coordinates.

Equations
@[simp]
theorem pi_Lp.equiv_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :
(λ (i : ι), 𝕜)) = a
@[simp]
theorem pi_Lp.equiv_symm_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :
((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm) a) =
@[simp]
theorem euclidean_space.single_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) (j : ι) :
= ite (j = i) a 0
theorem euclidean_space.inner_single_left {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) (v : ι) :
= a * v i
theorem euclidean_space.inner_single_right {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) (v : ι) :
= a * (star_ring_end ((λ (i : ι), 𝕜) i)) (v i)
@[simp]
theorem euclidean_space.norm_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :
@[simp]
theorem euclidean_space.nnnorm_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :
@[simp]
theorem euclidean_space.dist_single_same {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a b : 𝕜) :
=
@[simp]
theorem euclidean_space.nndist_single_same {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a b : 𝕜) :
@[simp]
theorem euclidean_space.edist_single_same {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a b : 𝕜) :
theorem euclidean_space.orthonormal_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] :
(λ (i : ι),

euclidean_space.single forms an orthonormal family.

theorem euclidean_space.pi_Lp_congr_left_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] {ι' : Type u_2} [fintype ι'] [decidable_eq ι'] (e : ι' ι) (i' : ι') (v : 𝕜) :
structure orthonormal_basis (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] (E : Type u_4) [ E] [fintype ι] :
Type (max u_1 u_3 u_4)

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

Instances for orthonormal_basis
@[protected, instance]
noncomputable def orthonormal_basis.inhabited {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] :
Equations
@[protected, instance]
noncomputable def orthonormal_basis.has_coe_to_fun {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] :
has_coe_to_fun E) (λ (_x : E), ι E)

b i is the ith basis vector.

Equations
@[simp]
theorem orthonormal_basis.coe_of_repr {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [decidable_eq ι] (e : E ≃ₗᵢ[𝕜] ) :
{repr := e} = λ (i : ι), (e.symm)
@[protected, simp]
theorem orthonormal_basis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [decidable_eq ι] (b : E) (i : ι) :
(b.repr.symm) = b i
@[protected, simp]
theorem orthonormal_basis.repr_self {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [decidable_eq ι] (b : E) (i : ι) :
(b.repr) (b i) =
@[protected]
theorem orthonormal_basis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) (v : E) (i : ι) :
(b.repr) v i = has_inner.inner (b i) v
@[protected, simp]
theorem orthonormal_basis.orthonormal {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) :
b
@[protected]
noncomputable def orthonormal_basis.to_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) :
𝕜 E

The basis ι 𝕜 E underlying the orthonormal_basis

Equations
@[protected, simp]
theorem orthonormal_basis.coe_to_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) :
@[protected, simp]
theorem orthonormal_basis.coe_to_basis_repr {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) :
@[protected, simp]
theorem orthonormal_basis.coe_to_basis_repr_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) (x : E) (i : ι) :
((b.to_basis.repr) x) i = (b.repr) x i
@[protected]
theorem orthonormal_basis.sum_repr {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) (x : E) :
finset.univ.sum (λ (i : ι), (b.repr) x i b i) = x
@[protected]
theorem orthonormal_basis.sum_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) (v : ι) :
finset.univ.sum (λ (i : ι), v i b i) = (b.repr.symm) v
@[protected]
theorem orthonormal_basis.sum_inner_mul_inner {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (b : E) (x y : E) :
finset.univ.sum (λ (i : ι), (b i) * has_inner.inner (b i) y) =
@[protected]
theorem orthonormal_basis.orthogonal_projection_eq_sum {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {U : E} (b : U) (x : E) :
= finset.univ.sum (λ (i : ι), has_inner.inner (b i) x b i)
@[protected]
noncomputable def orthonormal_basis.map {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {G : Type u_2} [ G] (b : E) (L : E ≃ₗᵢ[𝕜] G) :
G

Mapping an orthonormal basis along a linear_isometry_equiv.

Equations
@[protected, simp]
theorem orthonormal_basis.map_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {G : Type u_2} [ G] (b : E) (L : E ≃ₗᵢ[𝕜] G) (i : ι) :
(b.map L) i = L (b i)
@[protected, simp]
theorem orthonormal_basis.to_basis_map {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {G : Type u_2} [ G] (b : E) (L : E ≃ₗᵢ[𝕜] G) :
(b.map L).to_basis =
noncomputable def basis.to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :
E

A basis that is orthonormal is an orthonormal basis.

Equations
@[simp]
theorem basis.coe_to_orthonormal_basis_repr {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :
@[simp]
theorem basis.coe_to_orthonormal_basis_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :
@[simp]
theorem basis.to_basis_to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :
@[simp]
theorem basis.coe_to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :
@[protected]
noncomputable def orthonormal_basis.mk {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {v : ι E} (hon : v) (hsp : (set.range v)) :
E

A finite orthonormal set that spans is an orthonormal basis

Equations
@[protected, simp]
theorem orthonormal_basis.coe_mk {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {v : ι E} (hon : v) (hsp : (set.range v)) :
hsp) = v
@[protected]
noncomputable def orthonormal_basis.span {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [decidable_eq E] {v' : ι' E} (h : v') (s : finset ι') :

Any finite subset of a orthonormal family is an orthonormal_basis for its span.

Equations
@[protected, simp]
theorem orthonormal_basis.span_apply {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [decidable_eq E] {v' : ι' E} (h : v') (s : finset ι') (i : s) :
( i) = v' i
@[protected]
noncomputable def orthonormal_basis.mk_of_orthogonal_eq_bot {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {v : ι E} (hon : v) (hsp : (set.range v)) = ) :
E

A finite orthonormal family of vectors whose span has trivial orthogonal complement is an orthonormal basis.

Equations
@[protected, simp]
theorem orthonormal_basis.coe_of_orthogonal_eq_bot_mk {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {v : ι E} (hon : v) (hsp : (set.range v)) = ) :
= v
noncomputable def orthonormal_basis.reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [fintype ι'] (b : E) (e : ι ι') :
E

b.reindex (e : ι ≃ ι') is an orthonormal_basis indexed by ι'

Equations
@[protected]
theorem orthonormal_basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [fintype ι'] (b : E) (e : ι ι') (i' : ι') :
(b.reindex e) i' = b ((e.symm) i')
@[protected, simp]
theorem orthonormal_basis.coe_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [fintype ι'] (b : E) (e : ι ι') :
@[protected, simp]
theorem orthonormal_basis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [fintype ι'] (b : E) (e : ι ι') (x : E) (i' : ι') :
((b.reindex e).repr) x i' = (b.repr) x ((e.symm) i')
noncomputable def complex.orthonormal_basis_one_I  :

![1, I] is an orthonormal basis for ℂ considered as a real inner product space.

Equations
@[simp]
noncomputable def complex.isometry_of_orthonormal {F : Type u_6} (v : F) :

The isometry between ℂ and a two-dimensional real inner product space given by a basis.

Equations
@[simp]
theorem complex.map_isometry_of_orthonormal {F : Type u_6} {F' : Type u_7} [ F'] (v : F) (f : F ≃ₗᵢ[] F') :
theorem complex.isometry_of_orthonormal_apply {F : Type u_6} (v : F) (z : ) :
= z.re v 0 + z.im v 1

Matrix representation of an orthonormal basis with respect to another #

theorem orthonormal_basis.to_matrix_orthonormal_basis_mem_unitary {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [decidable_eq ι] (a b : E) :

The change-of-basis matrix between two orthonormal bases a, b is a unitary matrix.

@[simp]
theorem orthonormal_basis.det_to_matrix_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [decidable_eq ι] (a b : E) :

The determinant of the change-of-basis matrix between two orthonormal bases a, b has unit length.

theorem orthonormal_basis.to_matrix_orthonormal_basis_mem_orthogonal {ι : Type u_1} {F : Type u_6} [fintype ι] [decidable_eq ι] (a b : F) :

The change-of-basis matrix between two orthonormal bases a, b is an orthogonal matrix.

theorem orthonormal_basis.det_to_matrix_orthonormal_basis_real {ι : Type u_1} {F : Type u_6} [fintype ι] [decidable_eq ι] (a b : F) :

The determinant of the change-of-basis matrix between two orthonormal bases a, b is ±1.

Existence of orthonormal basis, etc. #

noncomputable def direct_sum.is_internal.collected_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {A : ι E} (hV : (λ (i : ι), (A i)) (λ (i : ι), (A i).subtypeₗᵢ)) [decidable_eq ι] (hV_sum : direct_sum.is_internal (λ (i : ι), A i)) {α : ι Type u_2} [Π (i : ι), fintype (α i)] (v_family : Π (i : ι), orthonormal_basis (α i) 𝕜 (A i)) :
orthonormal_basis (Σ (i : ι), α i) 𝕜 E

Given an internal direct sum decomposition of a module M, and an orthonormal basis for each of the components of the direct sum, the disjoint union of these orthonormal bases is an orthonormal basis for M.

Equations
theorem direct_sum.is_internal.collected_orthonormal_basis_mem {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] {A : ι E} [decidable_eq ι] (h : direct_sum.is_internal A) {α : ι Type u_2} [Π (i : ι), fintype (α i)] (hV : (λ (i : ι), (A i)) (λ (i : ι), (A i).subtypeₗᵢ)) (v : Π (i : ι), orthonormal_basis (α i) 𝕜 (A i)) (a : Σ (i : ι), α i) :
A a.fst
theorem orthonormal.exists_orthonormal_basis_extension {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] {v : set E} [ E] (hv : coe) :
{u : finset E} (b : E), v u

In a finite-dimensional inner_product_space, any orthonormal subset can be extended to an orthonormal basis.

theorem orthonormal.exists_orthonormal_basis_extension_of_card_eq {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [ E] {ι : Type u_1} [fintype ι] (card_ι : = ) {v : ι E} {s : set ι} (hv : (s.restrict v)) :
(b : E), (i : ι), i s b i = v i
theorem exists_orthonormal_basis (𝕜 : Type u_3) [is_R_or_C 𝕜] (E : Type u_4) [ E] [ E] :
(w : finset E) (b : E),

A finite-dimensional inner product space admits an orthonormal basis.

@[irreducible]
noncomputable def std_orthonormal_basis (𝕜 : Type u_3) [is_R_or_C 𝕜] (E : Type u_4) [ E] [ E] :
E

A finite-dimensional inner_product_space has an orthonormal basis.

Equations
• = let b : E := in _.mpr
theorem orthonormal_basis_one_dim {ι : Type u_1} [fintype ι] (b : ) :
(b = λ (_x : ι), 1) b = λ (_x : ι), -1

An orthonormal basis of ℝ is made either of the vector 1, or of the vector -1.

@[irreducible]
noncomputable def direct_sum.is_internal.sigma_orthonormal_basis_index_equiv {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [ E] {n : } (hn : = n) [decidable_eq ι] {V : ι E} (hV : direct_sum.is_internal V) (hV' : (λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :
(Σ (i : ι), fin (V i))) fin n

Exhibit a bijection between fin n and the index set of a certain basis of an n-dimensional inner product space E. This should not be accessed directly, but only via the subsequent API.

Equations
@[irreducible]
noncomputable def direct_sum.is_internal.subordinate_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [ E] {n : } (hn : = n) [decidable_eq ι] {V : ι E} (hV : direct_sum.is_internal V) (hV' : (λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :
𝕜 E

An n-dimensional inner_product_space equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by fin n and subordinate to that direct sum.

Equations
@[irreducible]
noncomputable def direct_sum.is_internal.subordinate_orthonormal_basis_index {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [ E] {n : } (hn : = n) [decidable_eq ι] {V : ι E} (hV : direct_sum.is_internal V) (a : fin n) (hV' : (λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :
ι

An n-dimensional inner_product_space equipped with a decomposition as an internal direct sum has an orthonormal basis indexed by fin n and subordinate to that direct sum. This function provides the mapping by which it is subordinate.

Equations
theorem direct_sum.is_internal.subordinate_orthonormal_basis_subordinate {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] [fintype ι] [ E] {n : } (hn : = n) [decidable_eq ι] {V : ι E} (hV : direct_sum.is_internal V) (a : fin n) (hV' : (λ (i : ι), (V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :
V

The basis constructed in orthogonal_family.subordinate_orthonormal_basis is subordinate to the orthogonal_family in question.

noncomputable def orthonormal_basis.from_orthogonal_span_singleton {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [ E] (n : ) [fact = n + 1)] {v : E} (hv : v 0) :
𝕜 {v})

Given a natural number n one less than the finrank of a finite-dimensional inner product space, there exists an isometry from the orthogonal complement of a nonzero singleton to euclidean_space 𝕜 (fin n).

Equations
noncomputable def linear_isometry.extend {𝕜 : Type u_3} [is_R_or_C 𝕜] {V : Type u_8} [ V] [ V] {S : V} (L : S →ₗᵢ[𝕜] V) :
V →ₗᵢ[𝕜] V

Let S be a subspace of a finite-dimensional complex inner product space V. A linear isometry mapping S into V can be extended to a full isometry of V.

TODO: The case when S is a finite-dimensional subspace of an infinite-dimensional V.

Equations
theorem linear_isometry.extend_apply {𝕜 : Type u_3} [is_R_or_C 𝕜] {V : Type u_8} [ V] [ V] {S : V} (L : S →ₗᵢ[𝕜] V) (s : S) :
(L.extend) s = L s
noncomputable def matrix.to_euclidean_lin {𝕜 : Type u_3} [is_R_or_C 𝕜] {m : Type u_8} {n : Type u_9} [fintype m] [fintype n] [decidable_eq n] :
n 𝕜 ≃ₗ[𝕜] →ₗ[𝕜]

matrix.to_lin' adapted for euclidean_space 𝕜 _.

Equations
@[simp]
theorem matrix.to_euclidean_lin_pi_Lp_equiv_symm {𝕜 : Type u_3} [is_R_or_C 𝕜] {m : Type u_8} {n : Type u_9} [fintype m] [fintype n] [decidable_eq n] (A : n 𝕜) (x : n 𝕜) :
(((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) x) = ((pi_Lp.equiv 2 (λ (ᾰ : m), 𝕜)).symm) ( x)
@[simp]
theorem matrix.pi_Lp_equiv_to_euclidean_lin {𝕜 : Type u_3} [is_R_or_C 𝕜] {m : Type u_8} {n : Type u_9} [fintype m] [fintype n] [decidable_eq n] (A : n 𝕜) (x : n) :
(λ (i : m), 𝕜)) x) = ( (λ (i : n), 𝕜)) x)
theorem matrix.to_euclidean_lin_eq_to_lin {𝕜 : Type u_3} [is_R_or_C 𝕜] {m : Type u_8} {n : Type u_9} [fintype m] [fintype n] [decidable_eq n] :
theorem inner_matrix_row_row {𝕜 : Type u_3} [is_R_or_C 𝕜] {m : Type u_8} {n : Type u_9} [fintype n] (A B : n 𝕜) (i j : m) :
has_inner.inner (((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) (A i)) (((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) (B j)) = j i

The inner product of a row of A and a row of B is an entry of B ⬝ Aᴴ.

theorem inner_matrix_col_col {𝕜 : Type u_3} [is_R_or_C 𝕜] {m : Type u_8} {n : Type u_9} [fintype m] (A B : n 𝕜) (i j : n) :
has_inner.inner (((pi_Lp.equiv 2 (λ (ᾰ : m), 𝕜)).symm) (A.transpose i)) (((pi_Lp.equiv 2 (λ (ᾰ : m), 𝕜)).symm) (B.transpose j)) = i j

The inner product of a column of A and a column of B is an entry of Aᴴ ⬝ B.