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

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.

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.
linear_isometry_equiv.of_inner_product_space: provides an arbitrary isometry to Euclidean space from a given finite-dimensional inner product space, induced by choosing an arbitrary basis.
complex.isometry_euclidean: standard isometry from ℂ to euclidean_space ℝ (fin 2)

source

@[protected, instance]

noncomputable def pi_Lp.inner_product_space {𝕜 : Type u_2} [is_R_or_C 𝕜] {ι : Type u_1} [fintype ι] (f : ι → Type u_3) [Π (i : ι), inner_product_space 𝕜 (f i)] :

inner_product_space 𝕜 (pi_Lp 2 f)

Equations

pi_Lp.inner_product_space f = {to_normed_group := pi_Lp.normed_group 2 f (λ (i : ι), inner_product_space.to_normed_group 𝕜), 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_sym := _, add_left := _, smul_left := _}

source

@[simp]

theorem pi_Lp.inner_apply {𝕜 : Type u_2} [is_R_or_C 𝕜] {ι : Type u_1} [fintype ι] {f : ι → Type u_3} [Π (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))

source

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

∥x∥ = real.sqrt (finset.univ.sum (λ (i : ι), ∥x i∥ ^ 2))

source

@[nolint]

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

source

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

∥x∥ = real.sqrt (finset.univ.sum (λ (i : n), ∥x i∥ ^ 2))

source

@[protected, instance]

def euclidean_space.finite_dimensional {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype ι] :

finite_dimensional 𝕜 (euclidean_space 𝕜 ι)

source

@[protected, instance]

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

inner_product_space 𝕜 (euclidean_space 𝕜 ι)

Equations

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

source

@[simp]

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

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

source

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

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

source

noncomputable def direct_sum.submodule_is_internal.isometry_L2_of_orthogonal_family {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.submodule_is_internal V) (hV' : orthogonal_family 𝕜 (λ (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.submodule_coe V) _ _ in (e₂.symm.trans e₁).isometry_of_inner _

source

@[simp]

theorem direct_sum.submodule_is_internal.isometry_L2_of_orthogonal_family_symm_apply {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [fintype ι] [decidable_eq ι] {V : ι → submodule 𝕜 E} (hV : direct_sum.submodule_is_internal V) (hV' : orthogonal_family 𝕜 (λ (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))

source

def euclidean_space.single {ι : Type u_1} {𝕜 : Type u_2} [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.single i a

source

@[simp]

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

euclidean_space.single i a j = ite (j = i) a 0

source

theorem euclidean_space.inner_single_left {ι : Type u_1} {𝕜 : Type u_2} [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

source

theorem euclidean_space.inner_single_right {ι : Type u_1} {𝕜 : Type u_2} [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)

source

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

Type (max u_1 u_2 u_3)

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

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

Instances for orthonormal_basis

source

@[protected, instance]

noncomputable def orthonormal_basis.inhabited {ι : Type u_1} {𝕜 : Type u_2} [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}}

source

@[protected, instance]

noncomputable def orthonormal_basis.has_coe_to_fun {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [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)}

source

@[protected, simp]

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

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

source

@[protected, simp]

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

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

source

@[protected]

theorem orthonormal_basis.repr_apply_apply {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) (v : E) (i : ι) :

⇑(b.repr) v i = has_inner.inner (⇑b i) v

source

@[protected, simp]

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

orthonormal 𝕜 ⇑b

source

@[protected]

noncomputable def orthonormal_basis.to_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [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

source

@[protected, simp]

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

⇑(b.to_basis) = ⇑b

source

@[protected, simp]

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

b.to_basis.equiv_fun = b.repr.to_linear_equiv

source

@[protected]

theorem orthonormal_basis.sum_repr_symm {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [fintype ι] (b : orthonormal_basis ι 𝕜 E) (v : euclidean_space 𝕜 ι) :

finset.univ.sum (λ (i : ι), v i • ⇑b i) = ⇑(b.repr.symm) v

source

noncomputable def basis.to_orthonormal_basis {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [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 _}

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

(v.to_orthonormal_basis hv).to_basis = v

source

@[simp]

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

⇑(v.to_orthonormal_basis hv) = ⇑v

source

@[protected]

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

orthonormal_basis ι 𝕜 E

An orthonormal set that spans is an orthonormal basis

Equations

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

source

@[protected, simp]

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

⇑(orthonormal_basis.mk hon hsp) = v

source

@[simp]

theorem basis.map_isometry_euclidean_of_orthonormal {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] {E' : Type u_4} [inner_product_space 𝕜 E'] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 ⇑v) (f : E ≃ₗᵢ[𝕜] E') :

((v.map f.to_linear_equiv).to_orthonormal_basis _).repr = f.symm.trans (v.to_orthonormal_basis hv).repr

If f : E ≃ₗᵢ[𝕜] E' is a linear isometry of inner product spaces then an orthonormal basis v of E determines a linear isometry e : E' ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι. This result states that e may be obtained either by transporting v to E' or by composing with the linear isometry E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι provided by v.

source

noncomputable def complex.isometry_euclidean :

ℂ ≃ₗᵢ[ℝ ] euclidean_space ℝ (fin 2)

ℂ is isometric to ℝ² with the Euclidean inner product.

Equations

complex.isometry_euclidean = (complex.basis_one_I.to_orthonormal_basis complex.isometry_euclidean._proof_1).repr

source

@[simp]

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

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

source

theorem complex.isometry_euclidean_proj_eq_self (z : ℂ) :

↑(⇑complex.isometry_euclidean z 0) + ↑(⇑complex.isometry_euclidean z 1) * is_R_or_C.I = z

source

@[simp]

theorem complex.isometry_euclidean_apply_zero (z : ℂ) :

⇑complex.isometry_euclidean z 0 = z.re

source

@[simp]

theorem complex.isometry_euclidean_apply_one (z : ℂ) :

⇑complex.isometry_euclidean z 1 = z.im

source

noncomputable def complex.isometry_of_orthonormal {F : Type u_5} [inner_product_space ℝ F] {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ ⇑v) :

ℂ ≃ₗᵢ[ℝ ] F

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

Equations

complex.isometry_of_orthonormal hv = complex.isometry_euclidean.trans (v.to_orthonormal_basis hv).repr.symm

source

@[simp]

theorem complex.map_isometry_of_orthonormal {F : Type u_5} [inner_product_space ℝ F] {F' : Type u_6} [inner_product_space ℝ F'] {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ ⇑v) (f : F ≃ₗᵢ[ℝ ] F') :

complex.isometry_of_orthonormal _ = (complex.isometry_of_orthonormal hv).trans f

source

theorem complex.isometry_of_orthonormal_symm_apply {F : Type u_5} [inner_product_space ℝ F] {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ ⇑v) (f : F) :

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

source

theorem complex.isometry_of_orthonormal_apply {F : Type u_5} [inner_product_space ℝ F] {v : basis (fin 2) ℝ F} (hv : orthonormal ℝ ⇑v) (z : ℂ) :

⇑(complex.isometry_of_orthonormal hv) z = z.re • ⇑v 0 + z.im • ⇑v 1

source

noncomputable def linear_isometry_equiv.of_inner_product_space {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] {n : ℕ} (hn : finite_dimensional.finrank 𝕜 E = n) :

E ≃ₗᵢ[𝕜] euclidean_space 𝕜 (fin n)

Given a natural number n equal to the finrank of a finite-dimensional inner product space, there exists an isometry from the space to euclidean_space 𝕜 (fin n).

Equations

linear_isometry_equiv.of_inner_product_space hn = ((fin_std_orthonormal_basis hn).to_orthonormal_basis _).repr

source

noncomputable def linear_isometry_equiv.from_orthogonal_span_singleton {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [inner_product_space 𝕜 E] (n : ℕ) [fact (finite_dimensional.finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :

↥(submodule.span 𝕜 {v})ᗮ ≃ₗᵢ[𝕜] euclidean_space 𝕜 (fin n)

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

linear_isometry_equiv.from_orthogonal_span_singleton n hv = linear_isometry_equiv.of_inner_product_space _

source

noncomputable def linear_isometry.extend {𝕜 : Type u_2} [is_R_or_C 𝕜] {V : Type u_7} [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 := L.to_linear_map.range, L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp (let BS : orthonormal_basis (fin d) 𝕜 ↥Sᗮ := (fin_std_orthonormal_basis linear_isometry.extend._proof_6).to_orthonormal_basis linear_isometry.extend._proof_7, BLS : orthonormal_basis (fin d) 𝕜 ↥LSᗮ := (fin_std_orthonormal_basis _).to_orthonormal_basis _ in BS.repr.trans BLS.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' := _}

source

theorem linear_isometry.extend_apply {𝕜 : Type u_2} [is_R_or_C 𝕜] {V : Type u_7} [inner_product_space 𝕜 V] [finite_dimensional 𝕜 V] {S : submodule 𝕜 V} (L : ↥S →ₗᵢ[𝕜] V) (s : ↥S) :

⇑(L.extend) ↑s = ⇑L s

source

theorem inner_matrix_row_row {𝕜 : Type u_2} [is_R_or_C 𝕜] {n m : ℕ} (A B : matrix (fin n) (fin m) 𝕜) (i j : fin n) :

has_inner.inner (A i) (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ᴴ.

source

theorem inner_matrix_col_col {𝕜 : Type u_2} [is_R_or_C 𝕜] {n m : ℕ} (A B : matrix (fin n) (fin m) 𝕜) (i j : fin m) :

has_inner.inner (A.transpose i) (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

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

Main definitions #

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