mathlib3 documentation

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 : ι), normed_add_comm_group (f i)] [Π (i : ι), inner_product_space 𝕜 (f i)] :

inner_product_space 𝕜 (pi_Lp 2 f)

Equations

pi_Lp.inner_product_space f = {to_normed_space := pi_Lp.normed_space 2 𝕜 f (λ (i : ι), inner_product_space.to_normed_space), to_has_inner := {inner := λ (x y : pi_Lp 2 f), finset.univ.sum (λ (i : ι), has_inner.inner (x i) (y i))}, norm_sq_eq_inner := _, conj_symm := _, add_left := _, smul_left := _}

@[simp]

theorem pi_Lp.inner_apply {𝕜 : Type u_3} [is_R_or_C 𝕜] {ι : Type u_1} [fintype ι] {f : ι → Type u_2} [Π (i : ι), normed_add_comm_group (f i)] [Π (i : ι), inner_product_space 𝕜 (f i)] (x y : pi_Lp 2 f) :

has_inner.inner x y = 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

euclidean_space 𝕜 n = pi_Lp 2 (λ (i : n), 𝕜)

theorem euclidean_space.nnnorm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x : euclidean_space 𝕜 n) :

‖x‖₊ = ⇑nnreal.sqrt (finset.univ.sum (λ (i : n), ‖x i‖₊ ^ 2))

theorem euclidean_space.norm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x : euclidean_space 𝕜 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 : euclidean_space 𝕜 n) :

has_dist.dist x y = √ (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 : euclidean_space 𝕜 n) :

has_nndist.nndist x y = ⇑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 : euclidean_space 𝕜 n) :

has_edist.edist x y = 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 ι] :

finite_dimensional 𝕜 (euclidean_space 𝕜 ι)

@[protected, instance]

noncomputable def euclidean_space.inner_product_space {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] :

inner_product_space 𝕜 (euclidean_space 𝕜 ι)

Equations

euclidean_space.inner_product_space = pi_Lp.inner_product_space (λ (i : ι), 𝕜)

@[simp]

theorem finrank_euclidean_space {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] :

finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 ι) = fintype.card ι

theorem finrank_euclidean_space_fin {𝕜 : Type u_3} [is_R_or_C 𝕜] {n : ℕ} :

finite_dimensional.finrank 𝕜 (euclidean_space 𝕜 (fin n)) = n

theorem euclidean_space.inner_eq_star_dot_product {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (x y : euclidean_space 𝕜 ι) :

has_inner.inner x y = matrix.dot_product (has_star.star (⇑(pi_Lp.equiv 2 (λ (i : ι), 𝕜)) x)) (⇑(pi_Lp.equiv 2 (λ (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) = matrix.dot_product (has_star.star x) 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V) (hV' : orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :

E ≃ₗᵢ[𝕜] pi_Lp 2 (λ (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

hV.isometry_L2_of_orthogonal_family hV' = let e₁ : direct_sum ι (λ (i : ι), (λ (i : ι), ↥(V i)) i) ≃ₗ[𝕜] Π (i : ι), (λ (i : ι), ↥(V i)) i := direct_sum.linear_equiv_fun_on_fintype 𝕜 ι (λ (i : ι), ↥(V i)), e₂ : direct_sum ι (λ (i : ι), ↥(V i)) ≃ₗ[𝕜] E := linear_equiv.of_bijective (direct_sum.coe_linear_map V) hV in (e₂.symm.trans e₁).isometry_of_inner _

@[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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V) (hV' : orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ)) (w : pi_Lp 2 (λ (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 ι] :

euclidean_space 𝕜 ι ≃L[𝕜] ι → 𝕜

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

Equations

euclidean_space.equiv ι 𝕜 = (pi_Lp.linear_equiv 2 𝕜 (λ (i : ι), 𝕜)).to_continuous_linear_equiv

@[simp]

theorem euclidean_space.equiv_to_linear_equiv_apply (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] (ᾰ : pi_Lp 2 (λ (i : ι), 𝕜)) (i : ι) :

⇑((euclidean_space.equiv ι 𝕜).to_linear_equiv) ᾰ i = ᾰ i

@[simp]

theorem euclidean_space.equiv_apply (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] (ᾰ : pi_Lp 2 (λ (i : ι), 𝕜)) (i : ι) :

⇑(euclidean_space.equiv ι 𝕜) ᾰ i = ᾰ i

@[simp]

theorem euclidean_space.equiv_symm_apply (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] [fintype ι] (ᾰ : Π (i : ι), (λ (i : ι), 𝕜) i) :

⇑((euclidean_space.equiv ι 𝕜).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) :

⇑((euclidean_space.equiv ι 𝕜).to_linear_equiv.symm) ᾰ = ⇑((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm) ᾰ

noncomputable def euclidean_space.projₗ {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) :

euclidean_space 𝕜 ι →ₗ[𝕜] 𝕜

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

Equations

euclidean_space.projₗ i = (linear_map.proj i).comp ↑(pi_Lp.linear_equiv 2 𝕜 (λ (i : ι), 𝕜))

@[simp]

theorem euclidean_space.projₗ_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) (ᾰ : euclidean_space 𝕜 ι) :

⇑(euclidean_space.projₗ i) ᾰ = ᾰ i

@[simp]

theorem euclidean_space.proj_coe {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) :

↑(euclidean_space.proj i) = euclidean_space.projₗ i

@[simp]

theorem euclidean_space.proj_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) (ᾰ : euclidean_space 𝕜 ι) :

⇑(euclidean_space.proj i) ᾰ = ᾰ i

noncomputable def euclidean_space.proj {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] (i : ι) :

euclidean_space 𝕜 ι →L[𝕜] 𝕜

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

Equations

euclidean_space.proj i = {to_linear_map := euclidean_space.projₗ i, cont := _}

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

euclidean_space 𝕜 ι

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

Equations

euclidean_space.single i a = ⇑((pi_Lp.equiv 2 (λ (i : ι), 𝕜)).symm) (pi.single i a)

@[simp]

theorem pi_Lp.equiv_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :

⇑(pi_Lp.equiv 2 (λ (i : ι), 𝕜)) (euclidean_space.single i a) = pi.single 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) (pi.single i a) = euclidean_space.single i a

@[simp]

theorem euclidean_space.single_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) (j : ι) :

euclidean_space.single 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 : euclidean_space 𝕜 ι) :

has_inner.inner (euclidean_space.single i a) v = ⇑(star_ring_end 𝕜) 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 : euclidean_space 𝕜 ι) :

has_inner.inner v (euclidean_space.single i a) = 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 : 𝕜) :

‖euclidean_space.single i a‖ = ‖a‖

@[simp]

theorem euclidean_space.nnnorm_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :

‖euclidean_space.single i a‖₊ = ‖a‖₊

@[simp]

theorem euclidean_space.dist_single_same {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a b : 𝕜) :

has_dist.dist (euclidean_space.single i a) (euclidean_space.single i b) = has_dist.dist 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 : 𝕜) :

has_nndist.nndist (euclidean_space.single i a) (euclidean_space.single i b) = has_nndist.nndist 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 : 𝕜) :

has_edist.edist (euclidean_space.single i a) (euclidean_space.single i b) = has_edist.edist a b

theorem euclidean_space.orthonormal_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] :

orthonormal 𝕜 (λ (i : ι), euclidean_space.single i 1)

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 : 𝕜) :

⇑(linear_isometry_equiv.pi_Lp_congr_left 2 𝕜 𝕜 e) (euclidean_space.single i' v) = euclidean_space.single (⇑e i') v

structure orthonormal_basis (ι : Type u_1) (𝕜 : Type u_3) [is_R_or_C 𝕜] (E : Type u_4) [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] :

Type (max u_1 u_3 u_4)

repr : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι

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 ι] :

inhabited (orthonormal_basis ι 𝕜 (euclidean_space 𝕜 ι))

Equations

orthonormal_basis.inhabited = {default := {repr := linear_isometry_equiv.refl 𝕜 (euclidean_space 𝕜 ι) normed_space.to_module}}

@[protected, instance]

noncomputable def orthonormal_basis.has_coe_to_fun {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] :

has_coe_to_fun (orthonormal_basis ι 𝕜 E) (λ (_x : orthonormal_basis ι 𝕜 E), ι → E)

b i is the ith basis vector.

Equations

orthonormal_basis.has_coe_to_fun = {coe := λ (b : orthonormal_basis ι 𝕜 E) (i : ι), ⇑(b.repr.symm) (euclidean_space.single i 1)}

@[simp]

theorem orthonormal_basis.coe_of_repr {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] (e : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι) :

⇑{repr := e} = λ (i : ι), ⇑(e.symm) (euclidean_space.single i 1)

@[protected, simp]

theorem orthonormal_basis.repr_symm_single {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] (b : orthonormal_basis ι 𝕜 E) (i : ι) :

⇑(b.repr.symm) (euclidean_space.single i 1) = ⇑b i

@[protected, simp]

theorem orthonormal_basis.repr_self {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] (b : orthonormal_basis ι 𝕜 E) (i : ι) :

⇑(b.repr) (⇑b i) = euclidean_space.single i 1

@[protected]

theorem orthonormal_basis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) :

orthonormal 𝕜 ⇑b

@[protected]

noncomputable def orthonormal_basis.to_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) :

basis ι 𝕜 E

The basis ι 𝕜 E underlying the orthonormal_basis

Equations

b.to_basis = basis.of_equiv_fun b.repr.to_linear_equiv

@[protected, simp]

theorem orthonormal_basis.coe_to_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) :

⇑(b.to_basis) = ⇑b

@[protected, simp]

theorem orthonormal_basis.coe_to_basis_repr {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) :

b.to_basis.equiv_fun = b.repr.to_linear_equiv

@[protected, simp]

theorem orthonormal_basis.coe_to_basis_repr_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) (v : euclidean_space 𝕜 ι) :

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) (x y : E) :

finset.univ.sum (λ (i : ι), has_inner.inner x (⇑b i) * has_inner.inner (⇑b i) y) = has_inner.inner x y

@[protected]

theorem orthonormal_basis.orthogonal_projection_eq_sum {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {U : submodule 𝕜 E} [complete_space ↥U] (b : orthonormal_basis ι 𝕜 ↥U) (x : E) :

⇑(orthogonal_projection U) x = 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {G : Type u_2} [normed_add_comm_group G] [inner_product_space 𝕜 G] (b : orthonormal_basis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) :

orthonormal_basis ι 𝕜 G

Mapping an orthonormal basis along a linear_isometry_equiv.

Equations

b.map L = {repr := L.symm.trans b.repr}

@[protected, simp]

theorem orthonormal_basis.map_apply {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {G : Type u_2} [normed_add_comm_group G] [inner_product_space 𝕜 G] (b : orthonormal_basis ι 𝕜 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {G : Type u_2} [normed_add_comm_group G] [inner_product_space 𝕜 G] (b : orthonormal_basis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G) :

(b.map L).to_basis = b.to_basis.map L.to_linear_equiv

noncomputable def basis.to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 ⇑v) :

orthonormal_basis ι 𝕜 E

A basis that is orthonormal is an orthonormal basis.

Equations

v.to_orthonormal_basis hv = {repr := v.equiv_fun.isometry_of_inner _}

@[simp]

theorem basis.coe_to_orthonormal_basis_repr {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 ⇑v) :

⇑((v.to_orthonormal_basis hv).repr) = ⇑(v.equiv_fun)

@[simp]

theorem basis.coe_to_orthonormal_basis_repr_symm {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 ⇑v) :

⇑((v.to_orthonormal_basis hv).repr.symm) = ⇑(v.equiv_fun.symm)

@[simp]

theorem basis.to_basis_to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 ⇑v) :

(v.to_orthonormal_basis hv).to_basis = v

@[simp]

theorem basis.coe_to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 ⇑v) :

⇑(v.to_orthonormal_basis hv) = ⇑v

@[protected]

noncomputable def orthonormal_basis.mk {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {v : ι → E} (hon : orthonormal 𝕜 v) (hsp : ⊤ ≤ submodule.span 𝕜 (set.range v)) :

orthonormal_basis ι 𝕜 E

A finite orthonormal set that spans is an orthonormal basis

Equations

orthonormal_basis.mk hon hsp = (basis.mk _ hsp).to_orthonormal_basis _

@[protected, simp]

theorem orthonormal_basis.coe_mk {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {v : ι → E} (hon : orthonormal 𝕜 v) (hsp : ⊤ ≤ submodule.span 𝕜 (set.range v)) :

⇑(orthonormal_basis.mk hon hsp) = v

@[protected]

noncomputable def orthonormal_basis.span {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [decidable_eq E] {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') :

orthonormal_basis ↥s 𝕜 ↥(submodule.span 𝕜 ↑(finset.image v' s))

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

Equations

orthonormal_basis.span h s = let e₀' : basis ↥s 𝕜 ↥(submodule.span 𝕜 (set.range (v' ∘ coe))) := basis.span _, e₀ : orthonormal_basis ↥s 𝕜 ↥(submodule.span 𝕜 (set.range (v' ∘ coe))) := orthonormal_basis.mk _ _, φ : ↥(submodule.span 𝕜 ↑(finset.image v' s)) ≃ₗᵢ[𝕜] ↥(submodule.span 𝕜 (set.range (v' ∘ coe))) := linear_isometry_equiv.of_eq (submodule.span 𝕜 ↑(finset.image v' s)) (submodule.span 𝕜 (set.range (v' ∘ coe))) _ in e₀.map φ.symm

@[protected, simp]

theorem orthonormal_basis.span_apply {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [decidable_eq E] {v' : ι' → E} (h : orthonormal 𝕜 v') (s : finset ι') (i : ↥s) :

↑(⇑(orthonormal_basis.span h 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {v : ι → E} (hon : orthonormal 𝕜 v) (hsp : (submodule.span 𝕜 (set.range v))ᗮ = ⊥) :

orthonormal_basis ι 𝕜 E

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

Equations

orthonormal_basis.mk_of_orthogonal_eq_bot hon hsp = orthonormal_basis.mk hon _

@[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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {v : ι → E} (hon : orthonormal 𝕜 v) (hsp : (submodule.span 𝕜 (set.range v))ᗮ = ⊥) :

⇑(orthonormal_basis.mk_of_orthogonal_eq_bot hon hsp) = v

noncomputable def orthonormal_basis.reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [fintype ι'] (b : orthonormal_basis ι 𝕜 E) (e : ι ≃ ι') :

orthonormal_basis ι' 𝕜 E

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

Equations

b.reindex e = {repr := b.repr.trans (linear_isometry_equiv.pi_Lp_congr_left 2 𝕜 𝕜 e)}

@[protected]

theorem orthonormal_basis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [fintype ι'] (b : orthonormal_basis ι 𝕜 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [fintype ι'] (b : orthonormal_basis ι 𝕜 E) (e : ι ≃ ι') :

⇑(b.reindex e) = ⇑b ∘ ⇑(e.symm)

@[protected, simp]

theorem orthonormal_basis.repr_reindex {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [fintype ι'] (b : orthonormal_basis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :

⇑((b.reindex e).repr) x i' = ⇑(b.repr) x (⇑(e.symm) i')

noncomputable def complex.orthonormal_basis_one_I :

orthonormal_basis (fin 2) ℝ ℂ

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

Equations

complex.orthonormal_basis_one_I = complex.basis_one_I.to_orthonormal_basis complex.orthonormal_basis_one_I._proof_1

@[simp]

theorem complex.orthonormal_basis_one_I_repr_apply (z : ℂ) :

⇑(complex.orthonormal_basis_one_I.repr) z = ![z.re, z.im]

@[simp]

theorem complex.orthonormal_basis_one_I_repr_symm_apply (x : euclidean_space ℝ (fin 2)) :

⇑(complex.orthonormal_basis_one_I.repr.symm) x = ↑(x 0) + ↑(x 1) * is_R_or_C.I

@[simp]

theorem complex.to_basis_orthonormal_basis_one_I :

complex.orthonormal_basis_one_I.to_basis = complex.basis_one_I

@[simp]

theorem complex.coe_orthonormal_basis_one_I :

⇑complex.orthonormal_basis_one_I = ![1, is_R_or_C.I]

noncomputable def complex.isometry_of_orthonormal {F : Type u_6} [normed_add_comm_group F] [inner_product_space ℝ F] (v : orthonormal_basis (fin 2) ℝ F) :

ℂ ≃ₗᵢ[ℝ ] F

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

Equations

complex.isometry_of_orthonormal v = complex.orthonormal_basis_one_I.repr.trans v.repr.symm

@[simp]

theorem complex.map_isometry_of_orthonormal {F : Type u_6} [normed_add_comm_group F] [inner_product_space ℝ F] {F' : Type u_7} [normed_add_comm_group F'] [inner_product_space ℝ F'] (v : orthonormal_basis (fin 2) ℝ F) (f : F ≃ₗᵢ[ℝ ] F') :

complex.isometry_of_orthonormal (v.map f) = (complex.isometry_of_orthonormal v).trans f

theorem complex.isometry_of_orthonormal_symm_apply {F : Type u_6} [normed_add_comm_group F] [inner_product_space ℝ F] (v : orthonormal_basis (fin 2) ℝ F) (f : F) :

⇑((complex.isometry_of_orthonormal v).symm) f = ↑(⇑(v.to_basis.coord 0) f) + ↑(⇑(v.to_basis.coord 1) f) * is_R_or_C.I

theorem complex.isometry_of_orthonormal_apply {F : Type u_6} [normed_add_comm_group F] [inner_product_space ℝ F] (v : orthonormal_basis (fin 2) ℝ F) (z : ℂ) :

⇑(complex.isometry_of_orthonormal v) 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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] (a b : orthonormal_basis ι 𝕜 E) :

a.to_basis.to_matrix ⇑b ∈ matrix.unitary_group ι 𝕜

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] (a b : orthonormal_basis ι 𝕜 E) :

‖⇑(a.to_basis.det) ⇑b‖ = 1

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} [normed_add_comm_group F] [inner_product_space ℝ F] [fintype ι] [decidable_eq ι] (a b : orthonormal_basis ι ℝ F) :

a.to_basis.to_matrix ⇑b ∈ matrix.orthogonal_group ι ℝ

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} [normed_add_comm_group F] [inner_product_space ℝ F] [fintype ι] [decidable_eq ι] (a b : orthonormal_basis ι ℝ F) :

⇑(a.to_basis.det) ⇑b = 1 ∨ ⇑(a.to_basis.det) ⇑b = -1

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {A : ι → submodule 𝕜 E} (hV : orthogonal_family 𝕜 (λ (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

direct_sum.is_internal.collected_orthonormal_basis hV hV_sum v_family = (hV_sum.collected_basis (λ (i : ι), (v_family i).to_basis)).to_orthonormal_basis _

theorem direct_sum.is_internal.collected_orthonormal_basis_mem {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] {A : ι → submodule 𝕜 E} [decidable_eq ι] (h : direct_sum.is_internal A) {α : ι → Type u_2} [Π (i : ι), fintype (α i)] (hV : orthogonal_family 𝕜 (λ (i : ι), ↥(A i)) (λ (i : ι), (A i).subtypeₗᵢ)) (v : Π (i : ι), orthonormal_basis (α i) 𝕜 ↥(A i)) (a : Σ (i : ι), α i) :

⇑(direct_sum.is_internal.collected_orthonormal_basis hV h v) a ∈ A a.fst

theorem orthonormal.exists_orthonormal_basis_extension {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] {v : set E} [finite_dimensional 𝕜 E] (hv : orthonormal 𝕜 coe) :

∃ {u : finset E} (b : orthonormal_basis ↥u 𝕜 E), v ⊆ ↑u ∧ ⇑b = coe

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {ι : Type u_1} [fintype ι] (card_ι : finite_dimensional.finrank 𝕜 E = fintype.card ι) {v : ι → E} {s : set ι} (hv : orthonormal 𝕜 (s.restrict v)) :

∃ (b : orthonormal_basis ι 𝕜 E), ∀ (i : ι), i ∈ s → ⇑b i = v i

theorem exists_orthonormal_basis (𝕜 : Type u_3) [is_R_or_C 𝕜] (E : Type u_4) [normed_add_comm_group E] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :

∃ (w : finset E) (b : orthonormal_basis ↥w 𝕜 E), ⇑b = coe

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) [normed_add_comm_group E] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :

orthonormal_basis (fin (finite_dimensional.finrank 𝕜 E)) 𝕜 E

A finite-dimensional inner_product_space has an orthonormal basis.

Equations

std_orthonormal_basis 𝕜 E = let b : orthonormal_basis ↥(classical.some _) 𝕜 E := classical.some _ in _.mpr (b.reindex (fintype.equiv_fin_of_card_eq _))

theorem orthonormal_basis_one_dim {ι : Type u_1} [fintype ι] (b : orthonormal_basis ι ℝ ℝ) :

(⇑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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V) (hV' : orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :

(Σ (i : ι), fin (finite_dimensional.finrank 𝕜 ↥(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

direct_sum.is_internal.sigma_orthonormal_basis_index_equiv hn hV hV' = let b : orthonormal_basis (Σ (i : ι), fin (finite_dimensional.finrank 𝕜 ↥(V i))) 𝕜 E := direct_sum.is_internal.collected_orthonormal_basis hV' hV (λ (i : ι), std_orthonormal_basis 𝕜 ↥(V i)) in fintype.equiv_fin_of_card_eq _

@[irreducible]

noncomputable def direct_sum.is_internal.subordinate_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V) (hV' : orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :

orthonormal_basis (fin n) 𝕜 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

direct_sum.is_internal.subordinate_orthonormal_basis hn hV hV' = (direct_sum.is_internal.collected_orthonormal_basis hV' hV (λ (i : ι), std_orthonormal_basis 𝕜 ↥(V i))).reindex (direct_sum.is_internal.sigma_orthonormal_basis_index_equiv hn hV hV')

@[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} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V) (a : fin n) (hV' : orthogonal_family 𝕜 (λ (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

direct_sum.is_internal.subordinate_orthonormal_basis_index hn hV a hV' = (⇑((direct_sum.is_internal.sigma_orthonormal_basis_index_equiv hn hV hV').symm) a).fst

theorem direct_sum.is_internal.subordinate_orthonormal_basis_subordinate {ι : Type u_1} {𝕜 : Type u_3} [is_R_or_C 𝕜] {E : Type u_4} [normed_add_comm_group E] [inner_product_space 𝕜 E] [fintype ι] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.is_internal V) (a : fin n) (hV' : orthogonal_family 𝕜 (λ (i : ι), ↥(V i)) (λ (i : ι), (V i).subtypeₗᵢ)) :

⇑(direct_sum.is_internal.subordinate_orthonormal_basis hn hV hV') a ∈ V (direct_sum.is_internal.subordinate_orthonormal_basis_index hn hV a hV')

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} [normed_add_comm_group E] [inner_product_space 𝕜 E] (n : ℕ) [fact (finite_dimensional.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :

orthonormal_basis (fin n) 𝕜 ↥(submodule.span 𝕜 {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

orthonormal_basis.from_orthogonal_span_singleton n hv = (std_orthonormal_basis 𝕜 ↥(submodule.span 𝕜 {v})ᗮ).reindex (fin_congr _)

noncomputable def linear_isometry.extend {𝕜 : Type u_3} [is_R_or_C 𝕜] {V : Type u_8} [normed_add_comm_group V] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] {S : submodule 𝕜 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

L.extend = let d : ℕ := finite_dimensional.finrank 𝕜 ↥Sᗮ, LS : submodule 𝕜 V := linear_map.range L.to_linear_map, L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp ((std_orthonormal_basis 𝕜 ↥Sᗮ).repr.trans ((std_orthonormal_basis 𝕜 ↥LSᗮ).reindex (fin_congr _)).repr.symm).to_linear_isometry, p1 : V →ₗ[𝕜] ↥S := (orthogonal_projection S).to_linear_map, p2 : V →ₗ[𝕜] ↥Sᗮ := (orthogonal_projection Sᗮ).to_linear_map, M : V →ₗ[𝕜] V := L.to_linear_map.comp p1 + L3.to_linear_map.comp p2 in {to_linear_map := M, norm_map' := _}

theorem linear_isometry.extend_apply {𝕜 : Type u_3} [is_R_or_C 𝕜] {V : Type u_8} [normed_add_comm_group V] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] {S : submodule 𝕜 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] :

matrix m n 𝕜 ≃ₗ[𝕜] euclidean_space 𝕜 n →ₗ[𝕜] euclidean_space 𝕜 m

matrix.to_lin' adapted for euclidean_space 𝕜 _.

Equations

matrix.to_euclidean_lin = matrix.to_lin'.trans ((pi_Lp.linear_equiv 2 𝕜 (λ (_x : n), 𝕜)).symm.arrow_congr (pi_Lp.linear_equiv 2 𝕜 (λ (_x : m), 𝕜)).symm)

@[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 : matrix m n 𝕜) (x : n → 𝕜) :

⇑(⇑matrix.to_euclidean_lin A) (⇑((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) x) = ⇑((pi_Lp.equiv 2 (λ (ᾰ : m), 𝕜)).symm) (⇑(⇑matrix.to_lin' A) 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 : matrix m n 𝕜) (x : euclidean_space 𝕜 n) :

⇑(pi_Lp.equiv 2 (λ (i : m), 𝕜)) (⇑(⇑matrix.to_euclidean_lin A) x) = ⇑(⇑matrix.to_lin' A) (⇑(pi_Lp.equiv 2 (λ (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] :

matrix.to_euclidean_lin = matrix.to_lin (pi_Lp.basis_fun 2 𝕜 n) (pi_Lp.basis_fun 2 𝕜 m)

theorem inner_matrix_row_row {𝕜 : Type u_3} [is_R_or_C 𝕜] {m : Type u_8} {n : Type u_9} [fintype n] (A B : matrix m n 𝕜) (i j : m) :

has_inner.inner (⇑((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) (A i)) (⇑((pi_Lp.equiv 2 (λ (ᾰ : n), 𝕜)).symm) (B j)) = B.mul A.conj_transpose 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 : matrix m 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)) = A.conj_transpose.mul B i j

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