mathlib documentation

analysis.inner_product_space.pi_L2

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

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

@[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)] :
Equations
@[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)
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)
@[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
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)
@[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 : } :
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 𝕜 V) :
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
@[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 𝕜 V) (w : pi_Lp 2 (λ (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} [inner_product_space 𝕜 E] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 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} [inner_product_space 𝕜 E] [fintype ι] (v : basis ι 𝕜 E) (hv : orthonormal 𝕜 v) :
@[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) :

is isometric to ℝ² with the Euclidean inner product.

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

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

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