Documentation

LeanPool.Monlib4.LinearAlgebra.Ips.TensorHilbert

Tensor product of inner product spaces #

Compatibility lemmas for Monlib's tensor-product inner-product API. The core inner product space structure now lives in Mathlib.

source
@[reducible, inline]
noncomputable abbrev TensorProduct.Inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] :
_root_.Inner 𝕜 (TensorProduct 𝕜 E F)

Compatibility alias for Monlib's named tensor-product inner structure.

Equations
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev TensorProduct.normedAddCommGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] :
    NormedAddCommGroup (TensorProduct 𝕜 E F)

    Compatibility alias for Monlib's named tensor-product normed additive group.

    Equations
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev TensorProduct.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] :
      InnerProductSpace 𝕜 (TensorProduct 𝕜 E F)

      Compatibility alias for Monlib's named tensor-product inner product space.

      Equations
      Instances For
        source
        theorem TensorProduct.inner_add_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x y z : TensorProduct 𝕜 E F) :
        inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z

        Inner products distribute over addition on the left in a tensor product.

        source
        theorem TensorProduct.inner_zero_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) :
        inner 𝕜 x 0 = 0

        The inner product with zero on the right is zero in a tensor product.

        source
        theorem TensorProduct.inner_conj_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x y : TensorProduct 𝕜 E F) :
        (starRingEnd 𝕜) (inner 𝕜 x y) = inner 𝕜 y x

        Conjugate symmetry of the tensor-product inner product.

        source
        theorem TensorProduct.inner_zero_left {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) :
        inner 𝕜 0 x = 0

        The inner product with zero on the left is zero in a tensor product.

        source
        theorem TensorProduct.inner_add_right {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x y z : TensorProduct 𝕜 E F) :
        inner 𝕜 x (y + z) = inner 𝕜 x y + inner 𝕜 x z

        Inner products distribute over addition on the right in a tensor product.

        source
        theorem TensorProduct.inner_sum {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {n : Type u_6} [Fintype n] (x : n → TensorProduct 𝕜 E F) (y : TensorProduct 𝕜 E F) :
        inner 𝕜 (∑ i : n, x i) y = ∑ i : n, inner 𝕜 (x i) y

        A finite sum in the left argument may be pulled out of the tensor-product inner product.

        source
        theorem TensorProduct.sum_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] {n : Type u_6} [Fintype n] (y : TensorProduct 𝕜 E F) (x : n → TensorProduct 𝕜 E F) :
        inner 𝕜 y (∑ i : n, x i) = ∑ i : n, inner 𝕜 y (x i)

        A finite sum in the right argument may be pulled out of the tensor-product inner product.

        source
        theorem TensorProduct.inner_nonneg_re {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) :
        0 ≤ RCLike.re (inner 𝕜 x x)

        The real part of ⟪x, x⟫ is nonnegative in a tensor product.

        source
        theorem TensorProduct.eq_span {𝕜 : Type u_6} {E : Type u_7} {F : Type u_8} [RCLike 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] (x : TensorProduct 𝕜 E F) :
        ∃ (α : ↑(Module.Basis.ofVectorSpaceIndex 𝕜 E) × ↑(Module.Basis.ofVectorSpaceIndex 𝕜 F) → E) (β : ↑(Module.Basis.ofVectorSpaceIndex 𝕜 E) × ↑(Module.Basis.ofVectorSpaceIndex 𝕜 F) → F), ∑ i : ↑(Module.Basis.ofVectorSpaceIndex 𝕜 E) × ↑(Module.Basis.ofVectorSpaceIndex 𝕜 F), α i ⊗ₜ[𝕜] β i = x

        A tensor-product element can be expanded as a finite sum of pure tensors.

        source
        theorem TensorProduct.lid_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
        LinearMap.adjoint ↑(TensorProduct.lid 𝕜 E) = ↑(TensorProduct.lid 𝕜 E).symm

        The adjoint of the left unitor is its inverse.

        source
        theorem TensorProduct.comm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] :
        LinearMap.adjoint ↑(TensorProduct.comm 𝕜 E F) = ↑(TensorProduct.comm 𝕜 E F).symm

        The adjoint of the symmetry is its inverse.

        source
        theorem TensorProduct.assoc_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] :
        LinearMap.adjoint ↑(TensorProduct.assoc 𝕜 E F G) = ↑(TensorProduct.assoc 𝕜 E F G).symm

        The adjoint of the associator is its inverse.

        source
        theorem TensorProduct.assoc_symm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] :
        LinearMap.adjoint ↑(TensorProduct.assoc 𝕜 E F G).symm = ↑(TensorProduct.assoc 𝕜 E F G)

        The adjoint of the inverse associator is the associator.

        source
        theorem TensorProduct.map_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] [FiniteDimensional 𝕜 G] [FiniteDimensional 𝕜 H] (f : E →ₗ[𝕜] F) (g : G →ₗ[𝕜] H) :
        LinearMap.adjoint (map f g) = map (LinearMap.adjoint f) (LinearMap.adjoint g)

        The adjoint of a tensor map is the tensor map of the adjoints.

        source
        theorem TensorProduct.lid_symm_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] :
        LinearMap.adjoint ↑(TensorProduct.lid 𝕜 E).symm = ↑(TensorProduct.lid 𝕜 E)

        The adjoint of the inverse left unitor is the left unitor.

        source
        theorem TensorProduct.comm_symm_adjoint {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [FiniteDimensional 𝕜 E] [FiniteDimensional 𝕜 F] :
        LinearMap.adjoint ↑(TensorProduct.comm 𝕜 E F).symm = ↑(TensorProduct.comm 𝕜 E F)

        The adjoint of the inverse symmetry is the symmetry.

        source
        theorem TensorProduct.inner_ext_iff' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x y : TensorProduct 𝕜 E F) :
        x = y ↔ ∀ (a : E) (b : F), inner 𝕜 x (a ⊗ₜ[𝕜] b) = inner 𝕜 y (a ⊗ₜ[𝕜] b)

        Equality of tensor-product elements can be tested against pure tensors.

        source
        theorem TensorProduct.inner_ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 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)

        Equality of pure tensors can be tested against pure tensors.

        source
        theorem TensorProduct.forall_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] (x : TensorProduct 𝕜 E F) :
        (∀ (a : E) (b : F), inner 𝕜 x (a ⊗ₜ[𝕜] b) = 0) ↔ x = 0

        A tensor is zero iff its inner product against every pure tensor is zero.

        source
        theorem TensorProduct.inner_ext_fourfold_iff' {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (x y : TensorProduct 𝕜 (TensorProduct 𝕜 E F) (TensorProduct 𝕜 G H)) :
        x = y ↔ ∀ (a : E) (b : F) (c : G) (d : H), inner 𝕜 x (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] (c ⊗ₜ[𝕜] d)) = inner 𝕜 y (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] (c ⊗ₜ[𝕜] d))

        Equality in a fourfold tensor product can be tested against pure tensors.

        source
        theorem TensorProduct.forall_fourfold_inner_eq_zero {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [NormedAddCommGroup G] [InnerProductSpace 𝕜 G] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) (TensorProduct 𝕜 G H)) :
        (∀ (a : E) (b : F) (c : G) (d : H), inner 𝕜 x (a ⊗ₜ[𝕜] b ⊗ₜ[𝕜] (c ⊗ₜ[𝕜] d)) = 0) ↔ x = 0

        A fourfold tensor is zero iff its inner product against every pure tensor is zero.