Prove2Me

bernoulli_powerset_expectation_linear

Proved

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

Linearity of the Bernoulli powerset expectation over a coordinate sum. For a statistic that is a sum of per-coordinate functions of the inclusion indicators,

E[∑wgw(1[w∈Ω])]=∑w(p gw(1)+(1−p) gw(0)).\mathbb{E}\Big[\sum_w g_w(\mathbf{1}[w\in\Omega])\Big] = \sum_w\big(p\,g_w(1)+(1-p)\,g_w(0)\big).

Each term reduces to its single-coordinate marginal. This is the form used to compute the mean of the centered sampling coefficient.

Preamble
import Definitions.Def_matrix_completion_neumann
open MatrixCompletion
open scoped BigOperators
Formal statement
theorem bernoulli_powerset_expectation_linear {n₁ n₂ : ℕ} (p : ℝ)
    (g : (Fin n₁ × Fin n₂) → ℝ → ℝ) :
    bernoulliExpectation p
        (fun Omega => ∑ w : Fin n₁ × Fin n₂, g w (if w ∈ Omega then 1 else 0)) =
      ∑ w : Fin n₁ × Fin n₂, (p * g w 1 + (1 - p) * g w 0) := by sorry
Source
Boucheron–Lugosi–Massart, Concentration Inequalities (OUP 2013), Ch. 15; foundational independence of coordinate inclusions under the product-Bernoulli powerset measure, used for the q-moment Bernstein estimate in Candès–Recht 2009, arXiv:0805.4471, §6.

View graph