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) :
has_inner.inner x y = finset.univ.sum (λ (i : ι), has_inner.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 (finset.univ.sum (λ (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 (finset.univ.sum (λ (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 𝕜 (λ (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
@[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))
def euclidean_space.single {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) :

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

Equations
@[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
theorem euclidean_space.inner_single_left {ι : Type u_1} {𝕜 : Type u_2} [is_R_or_C 𝕜] [fintype ι] [decidable_eq ι] (i : ι) (a : 𝕜) (v : euclidean_space 𝕜 ι) :
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)
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)

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_2} [is_R_or_C 𝕜] [fintype ι] :
Equations
@[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
@[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 : ι) :
@[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 : ι) :
@[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
@[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) :
@[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
@[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) :
@[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) :
@[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
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) :

A basis that is orthonormal is an orthonormal basis.

Equations
@[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) :
@[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) :
@[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) :
@[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) :
@[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) = ) :

An orthonormal set that spans is an orthonormal basis

Equations
@[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) = ) :
@[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') :

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.

is isometric to ℝ² with the Euclidean inner product.

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

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

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

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

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