theorem LiebAndoTrace.instNonnegSpectrumClassRealMulOppositeL {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : NonnegSpectrumClass ℝ (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ

theorem LiebAndoTrace.instIsometricContinuousFunctionalCalculusComplexMulOppositeLIsStarNormal {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : IsometricContinuousFunctionalCalculus ℂ (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ IsStarNormal

instance LiebAndoTrace.instCFCRealSelfAdjointMop {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ)ᵐᵒᵖ IsSelfAdjoint

noncomputable def LiebAndoTrace.traceRe {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] (T : LownerHeinzTheorem.L ℋ) : ℝ

The real part of the finite-dimensional trace on bounded operators.

Equations

• LiebAndoTrace.traceRe T = ((LinearMap.trace ℂ ℋ) ↑T).re

noncomputable def LiebAndoTrace.liebTraceMap {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (s : ℝ) (K A B : LownerHeinzTheorem.L ℋ) : ℝ

Trace functional appearing in Lieb's concavity theorem.

Equations

• LiebAndoTrace.liebTraceMap s K A B = LiebAndoTrace.traceRe (A ^ s * star K * B ^ (1 - s) * K)

noncomputable def LiebAndoTrace.liebExtensionTraceMap {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (q p : ℝ) (K A B : LownerHeinzTheorem.L ℋ) : ℝ

Trace functional appearing in Lieb's extension theorem.

Equations

• LiebAndoTrace.liebExtensionTraceMap q p K A B = LiebAndoTrace.traceRe (A ^ q * star K * B ^ p * K)

noncomputable def LiebAndoTrace.liebCorollaryTraceMap {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (q r : ℝ) (K A B : LownerHeinzTheorem.L ℋ) : ℝ

Trace functional appearing in Corollary 1.3.

Equations

• LiebAndoTrace.liebCorollaryTraceMap q r K A B = LiebAndoTrace.traceRe (A ^ q * star K * B ^ (1 - r) * K)

noncomputable def LiebAndoTrace.andoTraceMap {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (q r : ℝ) (K A B : LownerHeinzTheorem.L ℋ) : ℝ

Trace functional appearing in Ando's convexity theorem.

Equations

• LiebAndoTrace.andoTraceMap q r K A B = LiebAndoTrace.traceRe (A ^ q * star K * B ^ (-r) * K)

theorem LiebAndoTrace.pdSet_convexCombo {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {A B : LownerHeinzTheorem.L ℋ} {t : ℝ} (hA : A ∈ GeneralizedPerspectiveFunction.pdSet) (hB : B ∈ GeneralizedPerspectiveFunction.pdSet) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : (1 - t) • A + t • B ∈ GeneralizedPerspectiveFunction.pdSet

Convex combinations preserve pdSet (strict positivity).

theorem LiebAndoTrace.liebTrace_jointlyConcaveOn_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [Nontrivial ℋ] {s : ℝ} (hs0 : 0 < s) (hs1 : s < 1) (K : LownerHeinzTheorem.L ℋ) : GeneralizedPerspectiveFunction.JointlyConcaveOn GeneralizedPerspectiveFunction.pdSet GeneralizedPerspectiveFunction.pdSet (liebTraceMap s K)

theorem LiebAndoTrace.liebTrace_jointlyConvexOn_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [Nontrivial ℋ] {s : ℝ} (hs1 : 1 ≤ s) (hs2 : s ≤ 2) (K : LownerHeinzTheorem.L ℋ) : GeneralizedPerspectiveFunction.JointlyConvexOn GeneralizedPerspectiveFunction.pdSet GeneralizedPerspectiveFunction.pdSet (liebTraceMap s K)

theorem LiebAndoTrace.liebExtensionTrace_jointlyConcaveOn_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [Nontrivial ℋ] {p q : ℝ} (hp : 0 < p) (hq : 0 < q) (hpq : p + q ≤ 1) (K : LownerHeinzTheorem.L ℋ) : GeneralizedPerspectiveFunction.JointlyConcaveOn GeneralizedPerspectiveFunction.pdSet GeneralizedPerspectiveFunction.pdSet (liebExtensionTraceMap q p K)

theorem LiebAndoTrace.andoTrace_jointlyConvexOn_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [Nontrivial ℋ] {q r : ℝ} (hq1 : 1 ≤ q) (hq2 : q ≤ 2) (hr0 : 0 ≤ r) (hr1 : r ≤ 1) (hqr : 1 ≤ q - r) (K : LownerHeinzTheorem.L ℋ) : GeneralizedPerspectiveFunction.JointlyConvexOn GeneralizedPerspectiveFunction.pdSet GeneralizedPerspectiveFunction.pdSet (andoTraceMap q r K)

theorem LiebAndoTrace.liebCorollaryTrace_jointlyConvexOn_pdSet {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [FiniteDimensional ℂ ℋ] [Nontrivial ℋ] {q r : ℝ} (hr1 : 1 < r) (hrq : r ≤ q) (hq2 : q ≤ 2) (K : LownerHeinzTheorem.L ℋ) : GeneralizedPerspectiveFunction.JointlyConvexOn GeneralizedPerspectiveFunction.pdSet GeneralizedPerspectiveFunction.pdSet (liebCorollaryTraceMap q r K)