Documentation

Monlib.LinearAlgebra.Ips.TensorHilbert

Tensor product of inner product spaces #

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

noncomputable instance TensorProduct.Inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] :
_root_.Inner 𝕜 (TensorProduct 𝕜 E F)
Equations
  • One or more equations did not get rendered due to their size.
theorem TensorProduct.inner_tmul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x z : E) (y w : F) :
inner (x ⊗ₜ[𝕜] y) (z ⊗ₜ[𝕜] w) = inner x z * inner y w
theorem TensorProduct.inner_add_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y z : TensorProduct 𝕜 E F) :
inner (x + y) z = inner x z + inner y z
theorem TensorProduct.inner_zero_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) :
inner x 0 = 0
theorem TensorProduct.inner_conj_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y : TensorProduct 𝕜 E F) :
(starRingEnd 𝕜) (inner x y) = inner y x
theorem TensorProduct.inner_zero_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) :
inner 0 x = 0
theorem TensorProduct.inner_add_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y z : TensorProduct 𝕜 E F) :
inner x (y + z) = inner x y + inner x z
theorem TensorProduct.inner_sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n : Type u_4} [Fintype n] (x : nTensorProduct 𝕜 E F) (y : TensorProduct 𝕜 E F) :
inner (∑ i : n, x i) y = i : n, inner (x i) y
theorem TensorProduct.sum_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] {n : Type u_4} [Fintype n] (y : TensorProduct 𝕜 E F) (x : nTensorProduct 𝕜 E F) :
inner y (∑ i : n, x i) = i : n, inner y (x i)
theorem TensorProduct.inner_nonneg_re {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) :
theorem TensorProduct.eq_span {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) :
∃ (α : (Basis.ofVectorSpaceIndex 𝕜 E) × (Basis.ofVectorSpaceIndex 𝕜 F)E) (β : (Basis.ofVectorSpaceIndex 𝕜 E) × (Basis.ofVectorSpaceIndex 𝕜 F)F), i : (Basis.ofVectorSpaceIndex 𝕜 E) × (Basis.ofVectorSpaceIndex 𝕜 F), α i ⊗ₜ[𝕜] β i = x
@[reducible]
noncomputable instance TensorProduct.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] :
Equations
  • One or more equations did not get rendered due to their size.
theorem TensorProduct.inner_ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x z : E) (y w : F) :
x ⊗ₜ[𝕜] y = z ⊗ₜ[𝕜] w ∀ (a : E) (b : F), inner (x ⊗ₜ[𝕜] y) (a ⊗ₜ[𝕜] b) = inner (z ⊗ₜ[𝕜] w) (a ⊗ₜ[𝕜] b)
theorem TensorProduct.forall_inner_eq_zero {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) :
(∀ (a : E) (b : F), inner x (a ⊗ₜ[𝕜] b) = 0) x = 0
theorem TensorProduct.inner_ext_iff' {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [RCLike 𝕜] [NormedAddCommGroup E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x y : TensorProduct 𝕜 E F) :
x = y ∀ (a : E) (b : F), inner x (a ⊗ₜ[𝕜] b) = inner y (a ⊗ₜ[𝕜] b)