LeanPool.Monlib4.LinearAlgebra.QuantumSet.Instances

Imported Lean Pool material for LeanPool.Monlib4.LinearAlgebra.QuantumSet.Instances.

theorem Module.Dual.IsFaithfulPosMap.sig_trans_sig {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (x y : ℝ) : (hφ.sig x).trans (hφ.sig y) = hφ.sig (x + y)

theorem PosDef.smul {n : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {x : Matrix n n 𝕜} (hx : x.PosDef) (α : NNRealˣ) : (↑↑↑α • x).PosDef

theorem posSemidefOne_smul_rpow {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] (α : NNReal) (r : ℝ) : ⋯.rpow r = ↑(↑α ^ r) • 1

theorem posDefOne_smul_rpow {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] (α : NNRealˣ) (r : ℝ) : ⋯.rpow r = ↑(↑↑α ^ r) • 1

theorem Module.Dual.IsFaithfulPosMap.sig_zero {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : hφ.sig 0 = 1

theorem AlgEquiv.apply_eq_id {R : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring M] [Algebra R M] {f : M ≃ₐ[R] M} : (∀ (x : M), f x = x) ↔ f = 1

theorem Matrix.PosDef.rpow_neg_eq_inv_rpow {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝ) : hQ.rpow (-r) = (hQ.rpow r)⁻¹

theorem RCLike.pos_toNNReal_units {𝕜 : Type u_2} [RCLike 𝕜] (r : 𝕜) : 0 < r ↔ ∃ (s : NNRealˣ), r = ↑↑↑s

theorem RCLike.nonneg_toNNReal {𝕜 : Type u_2} [RCLike 𝕜] (r : 𝕜) : 0 ≤ r ↔ ∃ (s : NNReal), r = ↑↑s

theorem Matrix.smulPosDef_isPosDef_iff {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Finite n] [H : Nonempty n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : 𝕜) : (r • Q).PosDef ↔ 0 < r

theorem smul_onePosDef_rpow_eq {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {α : 𝕜} (h : (α • 1).PosDef) (r : ℝ) : h.rpow r = ↑(RCLike.re α ^ r) • 1

theorem Matrix.smulPosSemidef_isPosSemidef_iff {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Finite n] {Q : Matrix n n 𝕜} (hQ : Q.PosSemidef) (r : 𝕜) : (r • Q).PosSemidef ↔ 0 ≤ r ∨ Q = 0

theorem smul_onePosSemidef_rpow_eq {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {α : 𝕜} (h : (α • 1).PosSemidef) (r : ℝ) : h.rpow r = ↑(RCLike.re α ^ r) • 1

theorem Matrix.smulOneInv {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {s : NNRealˣ} : (↑↑↑s • 1)⁻¹ = ↑↑(↑s)⁻¹ • 1

theorem Matrix.PosDef.commutes_iff_rpow_commutes {𝕜 : Type u_2} [RCLike 𝕜] {n : Type u_3} [Fintype n] [DecidableEq n] {Q : Matrix n n 𝕜} (hQ : Q.PosDef) (r : ℝˣ) : (∀ (x : Matrix n n 𝕜), Commute x (hQ.rpow ↑r)) ↔ ∀ (x : Matrix n n 𝕜), Commute x Q

theorem Module.Dual.IsPosMap.isTracial_iff {n : Type u_2} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} (hφ : φ.IsPosMap) : φ.IsTracial ↔ ∃ (α : ℂ), φ.matrix = α • 1

theorem sig_eq_id_iff {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] (k : ℝ) : sig hφ k = 1 ↔ k = 0 ∨ φ.IsTracial

σ_k = 1 iff either k = 0 or φ is tracial

theorem Module.Dual.pi_isTracial_iff {k : Type u_2} [Fintype k] {s : k → Type u_3} [(i : k) → Fintype (s i)] {φ : (i : k) → Dual ℂ (Matrix (s i) (s i) ℂ)} : (pi φ).IsTracial ↔ ∀ (i : k), (φ i).IsTracial

@[reducible]

noncomputable def Matrix.isStarAlgebra {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : starAlgebra (Matrix n n ℂ)

The modular star-algebra structure on matrices induced by a faithful positive functional.

Equations

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

@[reducible]

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

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

@[reducible]

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

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

def «termWithMatrixQuantum[_]_» : Lean.ParserDescr

Elaborate a term using the matrix quantum-set structure induced by a faithful positive functional.

Equations

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

noncomputable def Module.Dual.IsFaithfulPosMap.psi {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Dual ℂ (Matrix n n ℂ)} {p : Type u_2} [Fintype p] [DecidableEq p] {ψ : Dual ℂ (Matrix p p ℂ)} (hφ : φ.IsFaithfulPosMap) [hψ : ψ.IsFaithfulPosMap] (t r : ℝ) : (Matrix n n ℂ →ₗ[ℂ] Matrix p p ℂ) ≃ₗ[ℂ] TensorProduct ℂ (Matrix p p ℂ) (Matrix n n ℂ)ᵐᵒᵖ

Matrix-specialized Psi equivalence for faithful positive functionals.

Equations

• hφ.psi t r = QuantumSet.Psi t r

noncomputable def piSig {k : Type u_2} {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) (z : ℝ) : PiMat ℂ k s ≃ₐ[ℂ] PiMat ℂ k s

Apply the modular automorphism to each matrix block in a family.

Equations

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

@[reducible]

noncomputable def PiMat.isStarAlgebra {k : Type u_2} {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)

The modular star-algebra structure on a finite product of matrix blocks.

Equations

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

@[reducible]

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)

Equations

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

@[reducible]

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

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

def «termWithPiQuantum[_]_» : Lean.ParserDescr

Elaborate a term using the product quantum-set structure induced by faithful positive functionals on matrix blocks.

Equations

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

theorem LinearMap.mul'_comp_mul'_adjoint_of_delta_form {n : Type u_1} [Fintype n] [DecidableEq n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : mul' ℂ (Matrix n n ℂ) ∘ₗ CoalgebraStruct.comul = φ.matrix⁻¹.trace • 1

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) → Module.Dual ℂ (Matrix (s i) (s i) ℂ)} [hφ : ∀ (i : k), (φ i).IsFaithfulPosMap] (hφ₂ : ∀ (i : k), (φ i).matrix⁻¹.trace = δ) : mul' ℂ (PiMat ℂ k s) ∘ₗ CoalgebraStruct.comul = δ • 1

theorem Qam.Nontracial.delta_pos {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : 0 < φ.matrix⁻¹.trace

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 = δ) : 0 < δ

@[reducible]

noncomputable def Matrix.quantumSetDeltaForm {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] {φ : Module.Dual ℂ (Matrix n n ℂ)} [hφ : φ.IsFaithfulPosMap] : QuantumSetDeltaForm (Matrix n n ℂ)

The delta-form quantum-set structure for a single matrix algebra.

Equations

• Matrix.quantumSetDeltaForm = { delta := φ.matrix⁻¹.trace, delta_pos := ⋯, mul_comp_comul_eq := ⋯ }

@[reducible]

noncomputable def 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)

The delta-form quantum-set structure for a finite product of matrix algebras.

Equations

• PiMat.quantumSetDeltaForm = { delta := d, delta_pos := ⋯, mul_comp_comul_eq := ⋯ }