Scalar Quantitative Logarithm Concavity

Proved

FunctionalInequalities.Analysis.scalar_log_gap_readable

by Lazyfill · Oct 26, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This lemma is a scalar inequality underlying a matrix log-determinant estimate.

For positive real numbers $a,b$ and an upper bound $K$ satisfying $a\le K$ and $b\le K$ ,

\log b+\frac{(b-a)^2}{2K^2}\le \log a+\frac{b-a}{a}.

The declaration scalar_log_gap_readable is a technical one-variable estimate. The hypotheses imply in particular that $K>0$ , although positivity of $K$ is not listed separately.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

private lemma scalar_log_gap {a b K : ℝ}
    (ha : 0 < a) (hb : 0 < b) (haK : a ≤ K) (hbK : b ≤ K) :
    Real.log b + (b - a) ^ 2 / (2 * K ^ 2) ≤
      Real.log a + (b - a) / a

Module navigation

Module: Analysis/Matrix/LogDet.

Previous: forall_posDef_add_log_det_le_trace_iff · Next: log_det_add_frobenius_sq_le.

Source excerpt, lines 150–153 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_LogDet

Formal statement

 lemma FunctionalInequalities.Analysis.scalar_log_gap_readable {a b K : ℝ}
    (ha : 0 < a) (hb : 0 < b) (haK : a ≤ K) (hbK : b ≤ K) :
    Real.log b + (b - a) ^ 2 / (2 * K ^ 2) ≤
      Real.log a + (b - a) / a := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/LogDet.lean#L150-L208 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.LogDet`, declaration `_private.FunctionalInequalities.Analysis.Matrix.LogDet.0.FunctionalInequalities.Analysis.scalar_log_gap`; the repository is private at upload time).

View graph