Bennett bound for one branch cumulant

Open

TalagrandCore.krL_le_bennett

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

concentration-inequalitiesempirical-processesprobabilitytalagrand

For a centered Bernoulli linear branch with coefficient envelope one and variance at most $\sigma^2$ , its negative-direction cumulant $L_a(t)$ satisfies, for $t\ge0$ ,

L_a(t)\le\sigma^2(e^t-t-1).

This is the single-branch Bennett estimate used to control the compensated process and the far lower-tail regime.

Formalization Note The branch cumulant is the sum of the exact one-coordinate Bernoulli cumulants.

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 krL_le_bennett {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) {coeff : ι → κ → ℝ}
    {a : ι} (hB : ∀ x, |coeff a x| ≤ 1) {sigmaSq : ℝ}
    (hVar : ∑ x : κ, p * (1 - p) * coeff a x ^ 2 ≤ sigmaSq) {t : ℝ} (ht : 0 ≤ t) :
    krL coeff p a t ≤ sigmaSq * (Real.exp t - t - 1) := 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