Prove2Me

Uniform Real Ceiling For Coercivity Expressions

Proved
FunctionalInequalities.Probability.MomentMeasure.real_coercivity_le_uniform_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is an elementary real-variable bound used to convert polynomial mass control into a finite ceiling.

For A,M∈RA,M\in\mathbb R, n∈Nn\in\mathbb N, and M≥0M\ge0,

log⁡A+nlog⁡max⁡{M,1}−M≤log⁡A+nlog⁡(2(n+1)).\log A+n\log\max\{M,1\}-M\le\log A+n\log\bigl(2(n+1)\bigr).

The estimate is valid for arbitrary real AA; only the nonnegativity of MM is assumed. It provides a finite upper bound independent of MM.

Original Lean declaration header

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

theorem real_coercivity_le_uniform (A : ℝ) (n : ℕ) (M : ℝ) (hM : 0 ≤ M) :
    Real.log A + (n : ℝ) * Real.log (max M 1) - M ≤
      Real.log A + (n : ℝ) * Real.log (2 * ((n : ℝ) + 1))

Module navigation

Module: Probability/MomentMeasure/Coercivity.

Previous: exists_integral_bound_of_eventual_functional_lower.

Source excerpt, lines 298–300 · Frozen source 408915f.

Preamble
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_MomentMeasure_Coercivity
Formal statement

theorem FunctionalInequalities.Probability.MomentMeasure.real_coercivity_le_uniform_readable (A : ℝ) (n : ℕ) (M : ℝ) (hM : 0 ≤ M) :
    Real.log A + (n : ℝ) * Real.log (max M 1) - M ≤
      Real.log A + (n : ℝ) * Real.log (2 * ((n : ℝ) + 1)) := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/MomentMeasure/Coercivity.lean#L297-L321 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.MomentMeasure.Coercivity`, declaration `FunctionalInequalities.Probability.MomentMeasure.real_coercivity_le_uniform`; the repository is private at upload time).

View graph