Klein–Rio Lemma 4.4: Bennett-kernel comparison

Proved

TalagrandCore.lemma44_consequence

by Harry_Xu · Aug 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

concentration-inequalitiesempirical-processesprobabilitytalagrand

For $t>0$ and $y\le1$ , the Bennett kernel obeys

(ty-1)e^{ty}+1\le y^2\bigl(1+(t-1)e^t\bigr).

This is the pointwise consequence of the monotonicity of $x^{-2}(1+(x-1)e^x)$ used in Klein–Rio’s lower-tail entropy argument.

Formalization Note The statement remains valid without a lower bound on $y$ .

Preamble

import Definitions.Def_talagrand_finite_bool_core
open MeasureTheory
open scoped Classical BigOperators

Formal statement

namespace TalagrandCore

variable {κ ι : Type} [DecidableEq κ] [Fintype κ]
variable [Fintype ι] [Nonempty ι]

theorem lemma44_consequence (t y : ℝ) (ht : 0 < t) (hy : y ≤ 1) :
    (t*y - 1) * Real.exp (t*y) + 1 ≤ y^2 * (1 + (t - 1) * Real.exp t) := by sorry

end TalagrandCore

Source

T. Klein and E. Rio, Concentration around the mean for maxima of empirical processes, Annals of Probability 33 (2005), Sections 2 and 4, pp. 1060–1077, arXiv:math/0506594. Formal Lean proof extracted from Prove2Me accepted submission bf106d23-ff42-48f5-a837-a8528101c849 by tianyipeng.

View graph