QuantumInfo.ForMathlib.HayataGroup.TraceInequality.JensenOperatorInequalityIImpIV

source

theorem JensenOperatorInequality.instContinuousFunctionalCalculusComplexProdLIsStarNormal {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] :

ContinuousFunctionalCalculus ℂ (LownerHeinzTheorem.L ℋ × LownerHeinzTheorem.L ℋ) IsStarNormal

source

theorem JensenOperatorInequality.instContinuousFunctionalCalculusRealProdLIsSelfAdjoint {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] :

ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ × LownerHeinzTheorem.L ℋ) IsSelfAdjoint

source

theorem JensenOperatorInequality.instNonnegSpectrumClassRealLHSum {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] :

NonnegSpectrumClass ℝ (LownerHeinzTheorem.L (HSum ℋ))

source

def JensenOperatorInequality.CondIV {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) :

Prop

Condition (iv) in Theorem 2.5.2.

Equations

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

Instances For

source

def JensenOperatorInequality.CondI {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) :

Prop

Condition (i) in Theorem 2.5.2 on the fixed Hilbert space ℋ.

Equations

JensenOperatorInequality.CondI f = (LownerHeinzTheorem.OperatorConvex f ∧ f 0 ≤ 0)

Instances For

source

def JensenOperatorInequality.CondIAll (f : ℝ → ℝ) :

Prop

Uniform version of Condition (i), packaged as OperatorConvexAll together with f 0 ≤ 0.

Equations

JensenOperatorInequality.CondIAll f = (LownerHeinzTheorem.OperatorConvexAll f ∧ f 0 ≤ 0)

Instances For

source

def JensenOperatorInequality.CondIciAll (f : ℝ → ℝ) :

Prop

Uniform localized version of Condition (i), packaged as OperatorConvexOnAll (Set.Ici 0) together with continuity and f 0 ≤ 0.

Equations

JensenOperatorInequality.CondIciAll f = (LownerHeinzTheorem.OperatorConvexOnAll (Set.Ici 0) f ∧ ContinuousOn f (Set.Ici 0) ∧ f 0 ≤ 0)

Instances For

source

def JensenOperatorInequality.CondV {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) :

Prop

Condition (v) in Theorem 2.5.2.

Equations

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

Instances For

source

theorem JensenOperatorInequality.theorem_2_5_2_i_ici_all_imp_iv {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f : ℝ → ℝ} (hf : CondIciAll f) :

CondIV f

source

theorem JensenOperatorInequality.theorem_2_5_2_i_all_imp_iv {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f : ℝ → ℝ} (hf : CondIAll f) :

CondIV f