Documentation

Monlib.LinearAlgebra.QuantumSet.SchurMul

Schur product operator #

In this file we define the Schur product operator and prove some basic properties.

Schur product ⬝ •ₛ ⬝ : (B → C) → (B → C) → (B → C) given by x •ₛ y := m ∘ (x ⊗ y) ∘ comul

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Schur product ⬝ •ₛ ⬝ : (B → C) → (B → C) → (B → C) given by x •ₛ y := m ∘ (x ⊗ y) ∘ comul

    Equations
    Instances For

      Pretty printer defined by notation3 command.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem schurMul.apply_rankOne {B : Type u_1} {C : Type u_2} [NormedAddCommGroupOfRing B] [NormedAddCommGroupOfRing C] [InnerProductSpace B] [InnerProductSpace C] [SMulCommClass B B] [SMulCommClass C C] [IsScalarTower B B] [IsScalarTower C C] [FiniteDimensional C] (a : B) (b : C) (c : B) (d : C) :
        (((rankOne ) a) b) •ₛ (((rankOne ) c) d) = (((rankOne ) (a * c)) (b * d))
        theorem schurMul.apply_ket {B : Type u_1} [NormedAddCommGroupOfRing B] [InnerProductSpace B] [SMulCommClass B B] [IsScalarTower B B] (a b : B) :
        ((ket ) a) •ₛ ((ket ) b) = ((ket ) (a * b))
        theorem bra_tmul {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (a : B) (b : C) :
        ((bra 𝕜) (a ⊗ₜ[𝕜] b)) = (TensorProduct.lid 𝕜 𝕜) ∘ₗ TensorProduct.map ((bra 𝕜) a) ((bra 𝕜) b)
        theorem bra_map_bra {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (a : B) (b : C) :
        TensorProduct.map ((bra 𝕜) a) ((bra 𝕜) b) = (TensorProduct.lid 𝕜 𝕜).symm ∘ₗ ((bra 𝕜) (a ⊗ₜ[𝕜] b))
        theorem ket_tmul {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (a : B) (b : C) :
        ((ket 𝕜) (a ⊗ₜ[𝕜] b)) = TensorProduct.map ((ket 𝕜) a) ((ket 𝕜) b) ∘ₗ (TensorProduct.lid 𝕜 𝕜).symm
        theorem ket_map_ket {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] (a : B) (b : C) :
        TensorProduct.map ((ket 𝕜) a) ((ket 𝕜) b) = ((ket 𝕜) (a ⊗ₜ[𝕜] b)) ∘ₗ (TensorProduct.lid 𝕜 𝕜)
        theorem rankOne_tmul {𝕜 : Type u_1} {B : Type u_2} {C : Type u_3} [RCLike 𝕜] [NormedAddCommGroup B] [NormedAddCommGroup C] [InnerProductSpace 𝕜 B] [InnerProductSpace 𝕜 C] [FiniteDimensional 𝕜 B] [FiniteDimensional 𝕜 C] {A : Type u_4} {D : Type u_5} [NormedAddCommGroup A] [NormedAddCommGroup D] [InnerProductSpace 𝕜 A] [InnerProductSpace 𝕜 D] [FiniteDimensional 𝕜 A] [FiniteDimensional 𝕜 D] (a : A) (b : B) (c : C) (d : D) :
        (((rankOne 𝕜) (a ⊗ₜ[𝕜] c)) (b ⊗ₜ[𝕜] d)) = TensorProduct.map (((rankOne 𝕜) a) b) (((rankOne 𝕜) c) d)
        theorem bra_comp_linearMap {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] [FiniteDimensional 𝕜 E₁] [FiniteDimensional 𝕜 E₂] (x : E₂) (f : E₁ →ₗ[𝕜] E₂) :
        ((bra 𝕜) x) ∘ₗ f = ((bra 𝕜) ((LinearMap.adjoint f) x))
        theorem linearMap_comp_ket {𝕜 : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E₁] [InnerProductSpace 𝕜 E₁] [NormedAddCommGroup E₂] [InnerProductSpace 𝕜 E₂] (x : E₁) (f : E₁ →ₗ[𝕜] E₂) :
        f ∘ₗ ((ket 𝕜) x) = ((ket 𝕜) (f x))
        theorem schurMul.apply_bra {C : Type u_1} [NormedAddCommGroupOfRing C] [InnerProductSpace C] [SMulCommClass C C] [IsScalarTower C C] [FiniteDimensional C] (a b : C) :
        ((bra ) a) •ₛ ((bra ) b) = ((bra ) (a * b))
        theorem schurMul_real {A : Type u_1} {B : Type u_2} [starAlgebra A] [starAlgebra B] [QuantumSet A] [QuantumSet B] (x y : A →ₗ[] B) :
        theorem schurMul_one_right_rankOne {B : Type u_1} [starAlgebra B] [hB : QuantumSet B] (a b : B) :
        theorem schurMul_one_left_rankOne {B : Type u_1} [starAlgebra B] [hB : QuantumSet B] (a b : B) :
        theorem Psi.schurMul {A : Type u_1} {B : Type u_2} [starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [QuantumSet B] (r₁ r₂ : ) (f g : A →ₗ[] B) :
        (QuantumSet.Psi r₁ r₂) (f •ₛ g) = (QuantumSet.Psi r₁ r₂) f * (QuantumSet.Psi r₁ r₂) g
        theorem schurMul_assoc {A : Type u_1} {B : Type u_2} [starAlgebra A] [starAlgebra B] [hA : QuantumSet A] [QuantumSet B] (f g h : A →ₗ[] B) :
        (f •ₛ g) •ₛ h = f •ₛ g •ₛ h