mathlib3 documentation

monlib / linear_algebra.my_ips.tensor_hilbert

Tensor product of inner product spaces #

This file constructs the tensor product of finite-dimensional inner product spaces.

@[protected, instance]

noncomputable def tensor_product.has_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] :

has_inner 𝕜 (tensor_product 𝕜 E F)

Equations

tensor_product.has_inner = {inner := λ (x y : tensor_product 𝕜 E F), let b₁ : orthonormal_basis (fin (finite_dimensional.finrank 𝕜 E)) 𝕜 E := std_orthonormal_basis 𝕜 E, b₂ : orthonormal_basis (fin (finite_dimensional.finrank 𝕜 F)) 𝕜 F := std_orthonormal_basis 𝕜 F in finset.univ.sum (λ (i : fin (finite_dimensional.finrank 𝕜 E)), finset.univ.sum (λ (j : fin (finite_dimensional.finrank 𝕜 F)), has_star.star (⇑(⇑((b₁.to_basis.tensor_product b₂.to_basis).repr) x) (i, j)) * ⇑(⇑((b₁.to_basis.tensor_product b₂.to_basis).repr) y) (i, j)))}

theorem tensor_product.inner_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x z : E) (y w : F) :

has_inner.inner (x ⊗ₜ[𝕜] y) (z ⊗ₜ[𝕜] w) = has_inner.inner x z * has_inner.inner y w

@[protected]

theorem tensor_product.inner_add_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x y z : tensor_product 𝕜 E F) :

has_inner.inner (x + y) z = has_inner.inner x z + has_inner.inner y z

@[protected]

theorem tensor_product.inner_zero_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x : tensor_product 𝕜 E F) :

has_inner.inner x 0 = 0

@[protected]

theorem tensor_product.inner_conj_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x y : tensor_product 𝕜 E F) :

⇑(star_ring_end 𝕜) (has_inner.inner x y) = has_inner.inner y x

@[protected]

theorem tensor_product.inner_zero_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x : tensor_product 𝕜 E F) :

has_inner.inner 0 x = 0

@[protected]

theorem tensor_product.inner_add_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x y z : tensor_product 𝕜 E F) :

has_inner.inner x (y + z) = has_inner.inner x y + has_inner.inner x z

@[protected]

theorem tensor_product.inner_sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] {n : Type u_4} [fintype n] (x : n → tensor_product 𝕜 E F) (y : tensor_product 𝕜 E F) :

has_inner.inner (finset.univ.sum (λ (i : n), x i)) y = finset.univ.sum (λ (i : n), has_inner.inner (x i) y)

@[protected]

theorem tensor_product.sum_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] {n : Type u_4} [fintype n] (y : tensor_product 𝕜 E F) (x : n → tensor_product 𝕜 E F) :

has_inner.inner y (finset.univ.sum (λ (i : n), x i)) = finset.univ.sum (λ (i : n), has_inner.inner y (x i))

@[protected]

theorem tensor_product.inner_nonneg_re {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x : tensor_product 𝕜 E F) :

0 ≤ ⇑is_R_or_C.re (has_inner.inner x x)

theorem tensor_product.eq_span {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [add_comm_group E] [module 𝕜 E] [add_comm_group F] [module 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x : tensor_product 𝕜 E F) :

∃ (α : ↥(basis.of_vector_space_index 𝕜 E) × ↥(basis.of_vector_space_index 𝕜 F) → E) (β : ↥(basis.of_vector_space_index 𝕜 E) × ↥(basis.of_vector_space_index 𝕜 F) → F), finset.univ.sum (λ (i : ↥(basis.of_vector_space_index 𝕜 E) × ↥(basis.of_vector_space_index 𝕜 F)), α i ⊗ₜ[𝕜] β i) = x

@[instance, reducible]

noncomputable def tensor_product.normed_add_comm_group {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] :

normed_add_comm_group (tensor_product 𝕜 E F)

Equations

tensor_product.normed_add_comm_group = inner_product_space.core.to_normed_add_comm_group

@[instance, reducible]

noncomputable def tensor_product.inner_product_space {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] :

inner_product_space 𝕜 (tensor_product 𝕜 E F)

Equations

tensor_product.inner_product_space = inner_product_space.of_core {to_has_inner := {inner := λ (x y : tensor_product 𝕜 E F), has_inner.inner x y}, conj_symm := _, nonneg_re := _, definite := _, add_left := _, smul_left := _}

theorem tensor_product.lid_adjoint {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :

⇑linear_map.adjoint ↑(tensor_product.lid 𝕜 E) = ↑((tensor_product.lid 𝕜 E).symm)

theorem tensor_product.comm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] :

⇑linear_map.adjoint ↑(tensor_product.comm 𝕜 E F) = ↑((tensor_product.comm 𝕜 E F).symm)

theorem tensor_product.assoc_symm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [inner_product_space 𝕜 G] [finite_dimensional 𝕜 G] :

⇑linear_map.adjoint ↑((tensor_product.assoc 𝕜 E F G).symm) = ↑(tensor_product.assoc 𝕜 E F G)

theorem tensor_product.assoc_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [inner_product_space 𝕜 G] [finite_dimensional 𝕜 G] :

⇑linear_map.adjoint ↑(tensor_product.assoc 𝕜 E F G) = ↑((tensor_product.assoc 𝕜 E F G).symm)

theorem tensor_product.map_adjoint {𝕜 : Type u_1} [is_R_or_C 𝕜] {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [normed_add_comm_group A] [normed_add_comm_group B] [normed_add_comm_group C] [normed_add_comm_group D] [inner_product_space 𝕜 A] [inner_product_space 𝕜 B] [inner_product_space 𝕜 C] [inner_product_space 𝕜 D] [finite_dimensional 𝕜 A] [finite_dimensional 𝕜 B] [finite_dimensional 𝕜 C] [finite_dimensional 𝕜 D] (f : A →ₗ[𝕜] B) (g : C →ₗ[𝕜] D) :

⇑linear_map.adjoint (tensor_product.map f g) = tensor_product.map (⇑linear_map.adjoint f) (⇑linear_map.adjoint g)

theorem tensor_product.inner_ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x z : E) (y w : F) :

x ⊗ₜ[𝕜] y = z ⊗ₜ[𝕜] w ↔ ∀ (a : E) (b : F), has_inner.inner (x ⊗ₜ[𝕜] y) (a ⊗ₜ[𝕜] b) = has_inner.inner (z ⊗ₜ[𝕜] w) (a ⊗ₜ[𝕜] b)

theorem tensor_product.forall_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x : tensor_product 𝕜 E F) :

(∀ (a : E) (b : F), has_inner.inner x (a ⊗ₜ[𝕜] b) = 0) ↔ x = 0

theorem tensor_product.inner_ext_iff' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group F] [inner_product_space 𝕜 E] [inner_product_space 𝕜 F] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 F] (x y : tensor_product 𝕜 E F) :

x = y ↔ ∀ (a : E) (b : F), has_inner.inner x (a ⊗ₜ[𝕜] b) = has_inner.inner y (a ⊗ₜ[𝕜] b)

theorem tensor_product.lid_symm_adjoint {𝕜 : Type u_1} {E : Type u_2} [is_R_or_C 𝕜] [normed_add_comm_group E] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :

⇑linear_map.adjoint (tensor_product.lid 𝕜 E).symm.to_linear_map = ↑(tensor_product.lid 𝕜 E)

theorem tensor_product.comm_symm_adjoint {𝕜 : Type u_1} {E : Type u_2} {V : Type u_3} [is_R_or_C 𝕜] [normed_add_comm_group E] [normed_add_comm_group V] [inner_product_space 𝕜 E] [inner_product_space 𝕜 V] [finite_dimensional 𝕜 E] [finite_dimensional 𝕜 V] :

⇑linear_map.adjoint (tensor_product.comm 𝕜 E V).symm.to_linear_map = ↑(tensor_product.comm 𝕜 E V)