mathlib documentation

analysis.inner_product_space.pi_L2

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 #

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
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) :
inner x y = ∑ (i : ι), 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 (∑ (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
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 (∑ (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
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
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 = ∑ (i : ι), ↑(w i)
source
noncomputable def basis.isometry_euclidean_of_orthonormal {ι : 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) :
E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι

An orthonormal basis on a fintype ι for an inner product space induces an isometry with euclidean_space 𝕜 ι.

Equations
source
@[simp]
theorem basis.coe_isometry_euclidean_of_orthonormal {ι : 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.isometry_euclidean_of_orthonormal hv) = ⇑(v.equiv_fun)
source
@[simp]
theorem basis.coe_isometry_euclidean_of_orthonormal_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.isometry_euclidean_of_orthonormal hv).symm) = ⇑(v.equiv_fun.symm)
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).isometry_euclidean_of_orthonormal _ = f.symm.trans (v.isometry_euclidean_of_orthonormal hv)

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