Equations
- QuantumGraph.Grad = { toFun := fun (f : B →ₗ[ℂ] B) => (LinearMap.rTensor B (LinearMap.adjoint f) - LinearMap.lTensor B f) ∘ₗ CoalgebraStruct.comul, map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
QuantumGraph.Grad_apply
{B : Type u_1}
[starAlgebra B]
[QuantumSet B]
(A : B →ₗ[ℂ] B)
:
Grad A = (LinearMap.rTensor B (LinearMap.adjoint A) - LinearMap.lTensor B A) ∘ₗ CoalgebraStruct.comul
theorem
QuantumGraph.Grad_eq
{B : Type u_1}
[starAlgebra B]
[QuantumSet B]
(gns : k B = 0)
(A : B →ₗ[ℂ] B)
:
Grad A = ↑(PhiMap A.real) ∘ₗ LinearMap.rTensor B (Algebra.linearMap ℂ B) ∘ₗ ↑(TensorProduct.lid ℂ B).symm - ↑(PhiMap A) ∘ₗ LinearMap.lTensor B (Algebra.linearMap ℂ B) ∘ₗ ↑(TensorProduct.rid ℂ B).symm
theorem
QuantumGraph.Real.range_grad_le_range_phiMap
{B : Type u_1}
[starAlgebra B]
[QuantumSet B]
(gns : k B = 0)
{A : B →ₗ[ℂ] B}
(hA : Real B A)
:
theorem
Upsilon_symm_grad_apply_apply
{B : Type u_1}
[starAlgebra B]
[QuantumSet B]
(gns : k B = 0)
(A : B →ₗ[ℂ] B)
(x : B)
:
theorem
QuantumGraph.apply_mul_of_isReal
{B : Type u_1}
[starAlgebra B]
[QuantumSet B]
(gns : k B = 0)
{A : B →ₗ[ℂ] B}
(hA : LinearMap.IsReal A)
(x y : B)
: