Prove2Me

centered_sampling_coefficient_second_moment

Proved

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

Exact second moment (variance) of the scalar centered sampling coefficient. For Coeff(Ω)=matrixEntrySum(centeredSamplingFluctuation(Ω,p,B))=∑ijp−1(1[(i,j)∈Ω]−p)Bij\mathrm{Coeff}(\Omega)=\texttt{matrixEntrySum}(\texttt{centeredSamplingFluctuation}(\Omega,p,B))=\sum_{ij}p^{-1}(\mathbf{1}[(i,j)\in\Omega]-p)B_{ij} and p≠0p\neq 0:

E[Coeff2]=1−pp ∥B∥F2.\mathbb{E}[\mathrm{Coeff}^2] = \frac{1-p}{p}\,\|B\|_F^2.

Proof: write Coeff=∑whw(1[w∈Ω])\mathrm{Coeff}=\sum_w h_w(\mathbf{1}[w\in\Omega]) with hw(x)=p−1Bw(x−p)h_w(x)=p^{-1}B_w(x-p); square to a double sum; push the expectation through both sums; the diagonal w=w′w=w' gives the single-coordinate second moment p hw(1)2+(1−p)hw(0)2=1−ppBw2p\,h_w(1)^2+(1-p)h_w(0)^2=\frac{1-p}{p}B_w^2, while every off-diagonal w≠w′w\neq w' term factorizes (pair independence) into a product of two single-coordinate means, each zero (centered terms). Only the diagonal survives. This is the variance σ2\sigma^2 input to the q-moment Bernstein estimate.

Preamble
import Definitions.Def_matrix_completion_neumann
open MatrixCompletion
open scoped BigOperators
Formal statement
theorem centered_sampling_coefficient_second_moment {n₁ n₂ : ℕ} (p : ℝ) (hp : p ≠ 0)
    (B : Matrix (Fin n₁) (Fin n₂) ℝ) :
    bernoulliExpectation p
      (fun Omega => (matrixEntrySum (centeredSamplingFluctuation Omega p B)) ^ 2) =
      ((1 - p) / p) * frobeniusNormSq B := 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