centered_sampling_coefficient_variance_bound

Proved

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

Variance bound $\sigma^2 \le \|B\|_F^2/p$ for the scalar centered sampling coefficient. From the exact second-moment identity $\mathbb{E}[\mathrm{Coeff}^2]=\frac{1-p}{p}\|B\|_F^2$ and $1-p\le 1$ (for $p\in(0,1]$ ) with $\|B\|_F^2\ge 0$ :

\mathbb{E}[\mathrm{Coeff}^2]=\frac{1-p}{p}\|B\|_F^2 \le \frac{\|B\|_F^2}{p}.

This is the $\sigma^2$ quantity fed (with $L\le\|B\|_\infty/p$ ) into the q-moment Bernstein estimate $\big(\mathbb{E}|\mathrm{Coeff}|^q\big)^{1/q}\le\sqrt{2q\sigma^2}+qL$ .

Preamble

import Definitions.Def_matrix_completion_neumann
open MatrixCompletion
open scoped BigOperators

Formal statement

theorem centered_sampling_coefficient_variance_bound {n₁ n₂ : ℕ} (p : ℝ)
    (hp0 : 0 < p) (hp1 : p ≤ 1) (B : Matrix (Fin n₁) (Fin n₂) ℝ) :
    bernoulliExpectation p
      (fun Omega => (matrixEntrySum (centeredSamplingFluctuation Omega p B)) ^ 2) ≤
      frobeniusNormSq B / p := by sorry

Source

Boucheron–Lugosi–Massart, Concentration Inequalities (OUP 2013), Ch. 15; Candès–Recht 2009, arXiv:0805.4471, §6 (centered sampling operator p⁻¹(P_Ω − p)).

View graph