The scalar tangent inequality

theorem CommutingRepetition.Resolver.negMulLog_le_tangent {x t : ℝ} (hx : 0 < x) (ht : 0 ≤ t) : t.negMulLog ≤ x.negMulLog + (-Real.log x - 1) * (t - x)

The tangent line of negMulLog at x > 0 dominates it on [0, ∞).

theorem CommutingRepetition.Resolver.smul_negMulLog_div_le {m y : ℝ} (hm0 : 0 < m) (hm1 : m ≤ 1) (hy : 0 ≤ y) : m * (y / m).negMulLog ≤ y.negMulLog

m · negMulLog (y / m) ≤ negMulLog y for 0 < m ≤ 1, 0 ≤ y.

The operator version

theorem CommutingRepetition.Resolver.continuousOn_negMulLog (s : Set ℝ) : ContinuousOn Real.negMulLog s

theorem CommutingRepetition.Resolver.cfc_negMulLog_le_affine {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) {x : ℝ} (hx : 0 < x) : cfc Real.negMulLog F ≤ (algebraMap ℝ A) (x.negMulLog - (-Real.log x - 1) * x) + (-Real.log x - 1) • F

The affine tangent bound as an operator inequality: for 0 ≤ F ≤ 1 and x > 0, H₁(F) ≼ (H₁(x) − s x)·1 + s F with s = −log x − 1.

theorem CommutingRepetition.Resolver.cfc_negMulLog_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {F : A} (hF0 : 0 ≤ F) (hF1 : F ≤ 1) : 0 ≤ cfc Real.negMulLog F

theorem CommutingRepetition.Resolver.jensen_negMulLog {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (ω : A →ₗ[ℝ] ℝ) (hmono : ∀ {a b : A}, a ≤ b → ω a ≤ ω b) (hm1 : ω 1 ≤ 1) {F : A} (hF0 : 0 ≤ F) (hF1 : F ≤ 1) : ω (cfc Real.negMulLog F) ≤ (ω F).negMulLog

Operator Jensen (eq positive-functional-jensen): for a positive real-linear functional ω with ω(1) ≤ 1 and a positive contraction F, ω(H₁(F)) ≤ H₁(ω(F)).