Bennett bound for one branch cumulant

Open

TalagrandCore.kr_cgf_le_bennett

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

bennett-inequalityconcentration-inequalitiesempirical-processesprobability

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 every $t\ge0$ ,

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

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

Formalization Note The branch cumulant is a finite sum of 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 kr_cgf_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), Lemma 4.4 and Section 4, pp. 1060–1077, arXiv:math/0506594. Formal Lean proof extracted from accepted submission bf106d23-ff42-48f5-a837-a8528101c849 by tianyipeng.

View graph