Prove2Me

bernoulli_powerset_expectation_pair_coordinate

Proved

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

Pair-coordinate independence of the Bernoulli powerset expectation. For two distinct coordinates w≠w′w\neq w', the expectation of a product of per-coordinate functions factorizes into the product of the two single-coordinate marginals:

E[g(1[w∈Ω]) h(1[w′∈Ω])]=(p g(1)+(1−p) g(0))(p h(1)+(1−p) h(0)).\mathbb{E}\big[g(\mathbf{1}[w\in\Omega])\,h(\mathbf{1}[w'\in\Omega])\big] = \big(p\,g(1)+(1-p)\,g(0)\big)\big(p\,h(1)+(1-p)\,h(0)\big).

This is the key input that makes the off-diagonal (cross) terms vanish when computing the variance / second moment of a statistic linear in the inclusion indicators, e.g. E[(∑waw(1[w∈Ω]−p))2]=∑waw2 p(1−p)\mathbb{E}[(\sum_w a_w(\mathbf{1}[w\in\Omega]-p))^2]=\sum_w a_w^2\,p(1-p). A direct consequence of the product-factorization (independence) lemma.

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

View graph