theorem HermitianMat.trace_cfc_conj_unitary {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (g : ℝ → ℝ) (U : ↥𝐔[d]) : (((conj ↑U) A).cfc g).trace = (A.cfc g).trace

The trace of cfc(g, A) is invariant under unitary conjugation of A. Follows from cfc_conj_unitary and trace_conj_unitary.

theorem HermitianMat.peierls_inequality {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (g : ℝ → ℝ) (hg : ConvexOn ℝ Set.univ g) : ∑ i : d, g (↑A i i).re ≤ (A.cfc g).trace

Peierls inequality: for a convex function g, the sum of g applied to the diagonal entries of a Hermitian matrix is at most the trace of g(A). This follows from Jensen's inequality applied to the spectral decomposition.

theorem HermitianMat.peierls_inequality_ici {d : Type u_1} [Fintype d] [DecidableEq d] (A : HermitianMat d ℂ) (g : ℝ → ℝ) (hg : ConvexOn ℝ (Set.Ici 0) g) (hA : 0 ≤ A) : ∑ i : d, g (↑A i i).re ≤ (A.cfc g).trace

theorem HermitianMat.trace_function_convex_univ {d : Type u_1} [Fintype d] [DecidableEq d] (g : ℝ → ℝ) (hg : ConvexOn ℝ Set.univ g) : ConvexOn ℝ Set.univ fun (A : HermitianMat d ℂ) => (A.cfc g).trace

Joint convexity of the trace functional: for a convex function g, the map A ↦ tr(g(A)) is convex on the space of Hermitian matrices.

theorem HermitianMat.trace_function_convex_ici {d : Type u_1} [Fintype d] [DecidableEq d] {g : ℝ → ℝ} (hg : ConvexOn ℝ (Set.Ici 0) g) : ConvexOn ℝ {A : HermitianMat d ℂ | 0 ≤ A} fun (A : HermitianMat d ℂ) => (A.cfc g).trace

Convexity of trace functions: if g is convex on ℝ₊, then A ↦ Tr[g(A)] is convex on PSD matrices.