theorem JensenOperatorInequality.instContinuousFunctionalCalculusComplexProdLIsStarNormal_1 {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : ContinuousFunctionalCalculus ℂ (LownerHeinzTheorem.L ℋ × LownerHeinzTheorem.L ℋ) IsStarNormal

theorem JensenOperatorInequality.instContinuousFunctionalCalculusRealProdLIsSelfAdjoint_1 {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : ContinuousFunctionalCalculus ℝ (LownerHeinzTheorem.L ℋ × LownerHeinzTheorem.L ℋ) IsSelfAdjoint

theorem JensenOperatorInequality.instNonnegSpectrumClassRealLHSum_1 {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : NonnegSpectrumClass ℝ (LownerHeinzTheorem.L (HSum ℋ))

@[implicit_reducible]

noncomputable def JensenOperatorInequality.instModuleRealLHSum {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : Module ℝ (LownerHeinzTheorem.L (HSum ℋ))

Equations

• JensenOperatorInequality.instModuleRealLHSum = inferInstance

def JensenOperatorInequality.CondIVAll (f : ℝ → ℝ) : Prop

Uniform version of Condition (iv), with the Hilbert space arbitrary in the same universe. This is the theorem-level uniform counterpart to the operator-level ...All predicates.

Equations

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

theorem JensenOperatorInequality.theorem_2_5_2_iv_imp_v {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f : ℝ → ℝ} (hiv : CondIVAll f) (hcont : ContinuousOn f Set.univ) : CondV f

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

Uniform consequence of Theorem 2.5.2: (i) → (v) via (iv).

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