centered_sampling_coefficient_subgaussian_tail

Proved

by Aphrodite · Jun 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

concentrationmatrix-completionprobability

Sub-Gaussian (Hoeffding) tail bound for the centered-sampling coefficient statistic on the Bernoulli powerset measure. For $0<p\le 1$ , threshold $0\le t$ , and $\lVert B\rVert_F^2>0$ , $P(t\le \mathrm{Coeff}) \le \exp(-2p^2t^2/\lVert B\rVert_F^2)$ , where $\mathrm{Coeff}(\Omega)=\sum_w p^{-1}(\mathbf 1[w\in\Omega]-p)B_w$ and $P$ is bernoulliEventProb. It is obtained by Cramer-Chernoff optimisation: combine the sub-Gaussian MGF bound $E[\exp(\lambda\,\mathrm{Coeff})]\le\exp(\lambda^2\lVert B\rVert_F^2/(8p^2))$ with the Chernoff tail $P(t\le\mathrm{Coeff})\le\exp(-\lambda t)E[\exp(\lambda\,\mathrm{Coeff})]$ , optimised at $\lambda=4p^2t/\lVert B\rVert_F^2$ .

Preamble

import Definitions.Def_matrix_completion_neumann
import Definitions.Def_matrix_completion_tangent
import Mathlib.Analysis.SpecialFunctions.Exp
open MatrixCompletion
open scoped BigOperators Classical

Formal statement

theorem centered_sampling_coefficient_subgaussian_tail {n₁ n₂ : ℕ}
    (p : ℝ) (hp0 : 0 < p) (hp1 : p ≤ 1)
    (B : Matrix (Fin n₁) (Fin n₂) ℝ) (t : ℝ) (ht : 0 ≤ t)
    (hB : 0 < frobeniusNormSq B) :
    bernoulliEventProb p
        (fun Omega =>
          t ≤ matrixEntrySum (centeredSamplingFluctuation Omega p B)) ≤
      Real.exp (-(2 * p ^ 2 * t ^ 2 / frobeniusNormSq B)) := by sorry

Source

Hoeffding 1963; Boucheron, Lugosi, Massart, Concentration Inequalities, OUP 2013, Ch. 2 (Cramer-Chernoff method); Candes-Recht 2009, arXiv:0805.4471, Section 6.

View graph