theorem
Module.Dual.IsFaithfulPosMap.sig_zero
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{φ : Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
:
theorem
Matrix.smulPosSemidef_isPosSemidef_iff
{𝕜 : Type u_2}
[RCLike 𝕜]
{n : Type u_3}
[Fintype n]
[DecidableEq n]
{Q : Matrix n n 𝕜}
(hQ : Q.PosSemidef)
(r : 𝕜)
:
theorem
smul_onePosSemidef_rpow_eq
{𝕜 : Type u_2}
[RCLike 𝕜]
{n : Type u_3}
[Fintype n]
[DecidableEq n]
{α : 𝕜}
(h : (α • 1).PosSemidef)
(r : ℝ)
:
theorem
sig_eq_id_iff
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{φ : Module.Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
(k : ℝ)
:
σ_k = 1
iff either k = 0
or φ
is tracial
@[defaultInstance 1000]
noncomputable instance
Matrix.isStarAlgebra
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{φ : Module.Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
:
starAlgebra (Matrix n n ℂ)
Equations
- Matrix.isStarAlgebra = starAlgebra.mk (sig hφ) ⋯ ⋯
noncomputable instance
Module.Dual.IsFaithfulPosMap.innerProductAlgebra
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{φ : Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
:
InnerProductAlgebra (Matrix n n ℂ)
Equations
noncomputable instance
Module.Dual.IsFaithfulPosMap.quantumSet
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{φ : Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
:
QuantumSet (Matrix n n ℂ)
Equations
noncomputable instance
PiMat.isStarAlgebra
{k : Type u_2}
[Fintype k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{ψ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)}
[_hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap]
:
starAlgebra (PiMat ℂ k s)
Equations
noncomputable instance
Module.Dual.pi.IsFaithfulPosMap.innerProductAlgebra
{k : Type u_2}
[Fintype k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)}
[∀ (i : k), (ψ i).IsFaithfulPosMap]
:
InnerProductAlgebra (PiMat ℂ k s)
noncomputable instance
Module.Dual.pi.IsFaithfulPosMap.quantumSet
{k : Type u_2}
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
{ψ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)}
[hψ : ∀ (i : k), (ψ i).IsFaithfulPosMap]
:
QuantumSet (PiMat ℂ k s)
Equations
- Module.Dual.pi.IsFaithfulPosMap.quantumSet = QuantumSet.mk ⋯ 0 ⋯ ⋯ ((i : k) × s i × s i) inferInstance inferInstance (Module.Dual.pi.IsFaithfulPosMap.orthonormalBasis hψ)
theorem
LinearMap.mul'_comp_mul'_adjoint_of_delta_form
{n : Type u_1}
[Fintype n]
[DecidableEq n]
{φ : Module.Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
:
theorem
LinearMap.pi_mul'_comp_mul'_adjoint_of_delta_form
{k : Type u_2}
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
[∀ (i : k), Nontrivial (s i)]
{δ : ℂ}
{φ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)}
[hφ : ∀ (i : k), (φ i).IsFaithfulPosMap]
(hφ₂ : ∀ (i : k), (φ i).matrix⁻¹.trace = δ)
:
theorem
Qam.Nontracial.delta_pos
{n : Type u_1}
[Fintype n]
[DecidableEq n]
[Nonempty n]
{φ : Module.Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
:
theorem
Pi.Qam.Nontracial.delta_ne_zero
{k : Type u_2}
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
[Nonempty k]
[∀ (i : k), Nontrivial (s i)]
{δ : ℂ}
{φ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)}
[hφ : ∀ (i : k), (φ i).IsFaithfulPosMap]
(hφ₂ : ∀ (i : k), (φ i).matrix⁻¹.trace = δ)
:
noncomputable instance
Matrix.quantumSetDeltaForm
{n : Type u_1}
[Fintype n]
[DecidableEq n]
[Nonempty n]
{φ : Module.Dual ℂ (Matrix n n ℂ)}
[hφ : φ.IsFaithfulPosMap]
:
QuantumSetDeltaForm (Matrix n n ℂ)
Equations
- Matrix.quantumSetDeltaForm = { delta := φ.matrix⁻¹.trace, delta_pos := ⋯, mul_comp_comul_eq := ⋯ }
noncomputable instance
PiMat.quantumSetDeltaForm
{k : Type u_2}
[Fintype k]
[DecidableEq k]
{s : k → Type u_3}
[(i : k) → Fintype (s i)]
[(i : k) → DecidableEq (s i)]
[Nonempty k]
[∀ (i : k), Nontrivial (s i)]
{d : ℂ}
{φ : (i : k) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)}
[hφ : ∀ (i : k), (φ i).IsFaithfulPosMap]
[hφ₂ : Fact (∀ (i : k), (φ i).matrix⁻¹.trace = d)]
:
QuantumSetDeltaForm (PiMat ℂ k s)
Equations
- PiMat.quantumSetDeltaForm = { delta := d, delta_pos := ⋯, mul_comp_comul_eq := ⋯ }