Real trace pairing for finite matrix operators

This module records the continuous real-linear trace pairing X ↦ Re Tr(ZX), the representation of every continuous real-linear functional by such a pairing, and the finite-dimensional Hilbert--Schmidt positivity facts used in weak duality and complementary slackness.

@[instance_reducible]

noncomputable def MIPStarRE.Quantum.instDecidableEq_mIPRE_1 {d : Type u_1} : DecidableEq d

Equations

• MIPStarRE.Quantum.instDecidableEq_mIPRE_1 = Classical.decEq d

theorem MIPStarRE.Quantum.instNonnegSpectrumClassRealOp_1 {d : Type u_1} [Fintype d] : NonnegSpectrumClass ℝ (Op d)

theorem MIPStarRE.Quantum.instNonUnitalContinuousFunctionalCalculusRealOpIsSelfAdjoint_1 {d : Type u_1} [Fintype d] : NonUnitalContinuousFunctionalCalculus ℝ (Op d) IsSelfAdjoint

Real trace pairing

noncomputable def MIPStarRE.Quantum.realTracePairingCLM {d : Type u_2} [Fintype d] [DecidableEq d] (Z : Op d) : Op d →L[ℝ] ℝ

The continuous real-linear functional X ↦ Re Tr(ZX).

Equations

• MIPStarRE.Quantum.realTracePairingCLM Z = { toFun := fun (X : MIPStarRE.Quantum.Op d) => (Z * X).trace.re, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem MIPStarRE.Quantum.realTracePairingCLM_apply {d : Type u_2} [Fintype d] [DecidableEq d] (Z X : Op d) : (realTracePairingCLM Z) X = (Z * X).trace.re

theorem MIPStarRE.Quantum.realTracePairingCLM_single {d : Type u_2} [Fintype d] [DecidableEq d] (Z : Op d) (i j : d) (z : ℂ) : (realTracePairingCLM Z) (Matrix.single i j z) = (Z j i * z).re

The trace pairing against a single matrix unit reads the transposed coordinate of Z.

noncomputable def MIPStarRE.Quantum.tracePairingMatrixOfRealCLM {d : Type u_2} [Fintype d] [DecidableEq d] (ψ : StrongDual ℝ (Op d)) : Op d

The matrix representing a continuous real-linear functional under the real trace pairing.

Equations

• MIPStarRE.Quantum.tracePairingMatrixOfRealCLM ψ i j = ↑(ψ (Matrix.single j i 1)) - ↑(ψ (Matrix.single j i Complex.I)) * Complex.I

theorem MIPStarRE.Quantum.realTracePairingCLM_tracePairingMatrixOfRealCLM {d : Type u_2} [Fintype d] [DecidableEq d] (ψ : StrongDual ℝ (Op d)) : realTracePairingCLM (tracePairingMatrixOfRealCLM ψ) = ψ

Every continuous real-linear functional on finite complex matrices is a real trace pairing.

theorem MIPStarRE.Quantum.realTracePairingCLM_selfAdjointPart_apply_of_isHermitian {d : Type u_2} [Fintype d] [DecidableEq d] (Z : Op d) {X : Op d} (hX : Matrix.IsHermitian X) : (realTracePairingCLM ↑((selfAdjointPart ℝ) Z)) X = (realTracePairingCLM Z) X

On Hermitian inputs, the Hermitian part has the same real trace pairing.

noncomputable def MIPStarRE.Quantum.hermitianTracePairingMatrixOfRealCLM {d : Type u_2} [Fintype d] [DecidableEq d] (ψ : StrongDual ℝ (Op d)) : Op d

The Hermitian representative of a real-linear functional.

Equations

• MIPStarRE.Quantum.hermitianTracePairingMatrixOfRealCLM ψ = ↑((selfAdjointPart ℝ) (MIPStarRE.Quantum.tracePairingMatrixOfRealCLM ψ))

theorem MIPStarRE.Quantum.hermitianTracePairingMatrixOfRealCLM_isHermitian {d : Type u_2} [Fintype d] [DecidableEq d] (ψ : StrongDual ℝ (Op d)) : Matrix.IsHermitian (hermitianTracePairingMatrixOfRealCLM ψ)

The Hermitian representative is Hermitian.

theorem MIPStarRE.Quantum.hermitianTracePairingMatrixOfRealCLM_apply_of_isHermitian {d : Type u_2} [Fintype d] [DecidableEq d] (ψ : StrongDual ℝ (Op d)) {X : Op d} (hX : Matrix.IsHermitian X) : ψ X = (hermitianTracePairingMatrixOfRealCLM ψ * X).trace.re

On Hermitian inputs, the Hermitian representative gives the same functional.

theorem MIPStarRE.Quantum.trace_mul_nonneg_of_nonneg {d : Type u_1} [Fintype d] {A B : Op d} (hA : 0 ≤ A) (hB : 0 ≤ B) : 0 ≤ (A * B).trace.re

The real trace pairing of two positive semidefinite operators is nonnegative.

This is the finite-dimensional Hilbert-Schmidt positivity fact used in weak duality arguments: if (A,B\geq 0), then (\operatorname{Re}\operatorname{Tr}(AB)\geq 0).

theorem MIPStarRE.Quantum.nonneg_of_trace_mul_nonneg_of_isHermitian {d : Type u_1} [Fintype d] {A : Op d} (hA : Matrix.IsHermitian A) (htrace : ∀ (B : Op d), 0 ≤ B → 0 ≤ (A * B).trace.re) : 0 ≤ A

A Hermitian operator whose real trace pairing with every PSD operator is nonnegative is positive semidefinite.

theorem MIPStarRE.Quantum.trace_mul_nonneg_forall_nonneg_iff_of_isHermitian {d : Type u_1} [Fintype d] {A : Op d} (hA : Matrix.IsHermitian A) : (∀ (B : Op d), 0 ≤ B → 0 ≤ (A * B).trace.re) ↔ 0 ≤ A

For a Hermitian operator, nonnegativity is equivalent to nonnegative real trace pairing against every positive semidefinite operator.

theorem MIPStarRE.Quantum.mul_eq_zero_of_nonneg_of_trace_mul_eq_zero {d : Type u_1} [Fintype d] {A B : Op d} (hA : 0 ≤ A) (hB : 0 ≤ B) (htrace : (A * B).trace.re = 0) : A * B = 0

If two positive semidefinite operators have zero trace pairing, then their product is zero.

This is the finite-dimensional complementary-slackness algebra used after a zero duality gap has been obtained: for PSD operators A and B, the equality Re Tr(A * B) = 0 forces A * B = 0.