# mathlibdocumentation

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 #

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

• basis.isometry_euclidean_of_orthonormal: provides the isometry to Euclidean space from a given finite-dimensional inner product space, induced by a basis of the space.

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

@[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 : ι), (f i)] :
(pi_Lp 2 f)
Equations
@[simp]
theorem pi_Lp.inner_apply {𝕜 : Type u_2} [is_R_or_C 𝕜] {ι : Type u_1} [fintype ι] {f : ι → Type u_3} [Π (i : ι), (f i)] (x y : f) :
y = ∑ (i : ι), inner (x i) (y i)
theorem pi_Lp.norm_eq_of_L2 {𝕜 : Type u_2} [is_R_or_C 𝕜] {ι : Type u_1} [fintype ι] {f : ι → Type u_3} [Π (i : ι), (f i)] (x : f) :
x = real.sqrt (∑ (i : ι), x i ^ 2)
@[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
• = (λ (i : n), 𝕜)
theorem euclidean_space.norm_eq {𝕜 : Type u_1} [is_R_or_C 𝕜] {n : Type u_2} [fintype n] (x : n) :
x = real.sqrt (∑ (i : n), x i ^ 2)
@[protected, instance]
def euclidean_space.finite_dimensional {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype ι] :
@[protected, instance]
noncomputable def euclidean_space.inner_product_space {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype ι] :
Equations
@[simp]
theorem finrank_euclidean_space {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype ι] :
theorem finrank_euclidean_space_fin {𝕜 : Type u_2} [is_R_or_C 𝕜] {n : } :
(fin n)) = n
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} [ E] [fintype ι] [decidable_eq ι] {V : ι → E} (hV' : V) :
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.submodule_is_internal.isometry_L2_of_orthogonal_family_symm_apply {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [fintype ι] [decidable_eq ι] {V : ι → E} (hV' : V) (w : (λ (i : ι), (V i))) :
((hV.isometry_L2_of_orthogonal_family hV').symm) w = ∑ (i : ι), (w i)
noncomputable def basis.isometry_euclidean_of_orthonormal {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :

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

Equations
@[simp]
theorem basis.coe_isometry_euclidean_of_orthonormal {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :
@[simp]
theorem basis.coe_isometry_euclidean_of_orthonormal_symm {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [fintype ι] (v : 𝕜 E) (hv : v) :
noncomputable def complex.isometry_euclidean  :

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

Equations
@[simp]
theorem complex.isometry_euclidean_symm_apply (x : (fin 2)) :
= (x 0) + ((x 1)) * is_R_or_C.I
noncomputable def linear_isometry_equiv.of_inner_product_space {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] [ E] {n : } (hn : = n) :
E ≃ₗᵢ[𝕜] (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
noncomputable def linear_isometry_equiv.from_orthogonal_span_singleton {𝕜 : Type u_2} [is_R_or_C 𝕜] {E : Type u_3} [ E] (n : ) [fact = n + 1)] {v : E} (hv : v 0) :
{v}) ≃ₗᵢ[𝕜] (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