Boundedness From A Logarithmic Lower Bound

Proved

FunctionalInequalities.Probability.MomentMeasure.exists_bound_of_log_lower_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an elementary coercivity lemma for real parameters.

For $A,b\in\mathbb R$ and $n\in\mathbb N$ , there exists $B\ge0$ such that every $M\ge0$ satisfying

b\le\log A+n\log\max\{M,1\}-M

also satisfies

M\le B.

The conclusion converts a lower bound on the logarithmic coercivity expression into a uniform upper bound on $M$ .

Original Lean declaration header

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

theorem exists_bound_of_log_lower (A : ℝ) (n : ℕ) (b : ℝ) :
    ∃ B : ℝ, 0 ≤ B ∧ ∀ M : ℝ, 0 ≤ M →
      b ≤ Real.log A + (n : ℝ) * Real.log (max M 1) - M → M ≤ B

Module navigation

Module: Probability/MomentMeasure/Coercivity.

Previous: exists_coercivity_of_centered_probability · Next: exists_integral_bound_of_eventual_functional_lower.

Source excerpt, lines 213–215 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_Coercivity

Formal statement


theorem FunctionalInequalities.Probability.MomentMeasure.exists_bound_of_log_lower_readable (A : ℝ) (n : ℕ) (b : ℝ) :
    ∃ B : ℝ, 0 ≤ B ∧ ∀ M : ℝ, 0 ≤ M →
      b ≤ Real.log A + (n : ℝ) * Real.log (max M 1) - M → M ≤ B := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/MomentMeasure/Coercivity.lean#L211-L236 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.MomentMeasure.Coercivity`, declaration `FunctionalInequalities.Probability.MomentMeasure.exists_bound_of_log_lower`; the repository is private at upload time).

View graph