Main result for DPI

We derive the concavity of the trace functional σ ↦ Tr[(σ^s H σ^s)^p] from the Lieb–Ando trace inequalities proved in LiebAndoTrace.lean.

@[reducible, inline]

noncomputable abbrev HermitianMatBridge.Φ {d : Type u_1} [Fintype d] [DecidableEq d] : Matrix d d ℂ ≃⋆ₐ[ℂ] EuclideanSpace ℂ d →L[ℂ] EuclideanSpace ℂ d

Abbreviation for the star algebra isomorphism.

Equations

• HermitianMatBridge.Φ = Matrix.toEuclideanCLM

theorem HermitianMatBridge.Φ_continuous {d : Type u_1} [Fintype d] [DecidableEq d] : Continuous ⇑Φ

Φ is continuous (as a linear map between finite-dimensional spaces).

theorem HermitianMatBridge.Φ_isSelfAdjoint {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) : IsSelfAdjoint (Φ ↑A)

Φ maps Hermitian matrices to self-adjoint operators.

theorem HermitianMatBridge.Φ_nonneg {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : 0 ≤ A) : 0 ≤ Φ ↑A

theorem HermitianMatBridge.Φ_mem_pdSet {d : Type u_1} [Fintype d] [DecidableEq d] [Nonempty d] (A : HermitianMat d ℂ) (hA : (↑A).PosDef) : Φ ↑A ∈ GeneralizedPerspectiveFunction.pdSet

Φ maps PosDef HermitianMat to pdSet.

theorem HermitianMatBridge.Φ_cfc {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (f : ℝ → ℝ) : Φ (cfc f ↑A) = cfc f (Φ ↑A)

Φ commutes with CFC for Hermitian matrices.

theorem HermitianMatBridge.Φ_rpow {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (hA : 0 ≤ A) (r : ℝ) : Φ ↑(A ^ r) = Φ ↑A ^ r

Φ commutes with rpow for PSD matrices.

theorem HermitianMatBridge.trace_Φ_eq {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) : (LinearMap.trace ℂ (EuclideanSpace ℂ d)) ↑(Φ M) = M.trace

General trace bridge: the operator trace of Φ(M) equals the matrix trace of M, for any matrix M (not just Hermitian).

theorem HermitianMatBridge.traceRe_Φ_general {d : Type u_1} [Fintype d] [DecidableEq d] (M : Matrix d d ℂ) : LiebAndoTrace.traceRe (Φ M) = M.trace.re

traceRe(Φ(M)) = re(Tr[M]) for any matrix M.

Density and continuity lemmas for PD/PSD extension

Helper lemmas for the core concavity proof

Core concavity on positive definite matrices

theorem HermitianMat.trace_conj_rpow_concave {d : Type u_1} [Fintype d] [DecidableEq d] {α : ℝ} (hα : 1 < α) (H : HermitianMat d ℂ) (hH : 0 ≤ H) : ConcaveOn ℝ {σ : HermitianMat d ℂ | 0 ≤ σ} fun (σ : HermitianMat d ℂ) => ((conj ↑(σ ^ ((α - 1) / (2 * α)))) H ^ (α / (α - 1))).trace