Coordinate-sum Bennett bound for a Bernoulli branch cumulant

Open

TalagrandCore.kr_coordinate_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 total variance at most $\sigma^2$ , let $\ell_x(t)$ be the exact one-coordinate negative cumulant. For every $t\ge0$ ,

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

This coordinate-sum form is the additive Bennett estimate used in the far lower-tail argument and can be folded into any aggregate branch-cumulant notation.

Formalization Note The function krl is the logarithm of the exact one-coordinate Bernoulli moment-generating factor.

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_coordinate_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) :
    (∑ x : κ, krl coeff p a x 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