bernoulli_product_measure_coords_indep

Proved

by Aphrodite · Jun 23, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bernoulliindependencematrix-completionmeasure-theoryprobability

Coordinate independence of the product-Bernoulli sampling measure. The family of per-coordinate Bool indicators $(\omega \mapsto \omega(w))_{w}$ is iIndepFun (mutually independent) under bernMeasure p = Measure.pi of independent Bernoulli $(p)$ coordinates on $(\mathrm{Fin}\,n_1 \times \mathrm{Fin}\,n_2) \to \mathrm{Bool}$ . Together with the keystone bridge (bernoulliExpectation = integral against bernMeasure), this exposes the powerset sampling model's coordinate independence in Mathlib's stock ProbabilityTheory.iIndepFun form, so Mathlib's independence API (product of expectations, independent sums, condExp w.r.t. coordinate sub-sigma-algebras, Hoeffding/sub-Gaussian MGF) applies directly. Proof: iIndepFun_pi (coordinates of a Measure.pi are independent).

Preamble

import Definitions.Def_matrix_completion_bernoulli_measure
import Mathlib.Probability.Independence.Basic
open MatrixCompletion
open scoped BigOperators Classical
open MeasureTheory ProbabilityTheory

Formal statement

theorem bernoulli_product_measure_coords_indep
    {n1 n2 : ℕ} (p : NNReal) (hp : p ≤ 1) :
    iIndepFun (fun (w : Fin n1 × Fin n2) (ω : (Fin n1 × Fin n2) → Bool) => ω w)
      (bernMeasure p hp) := by sorry

Source

Mathlib Probability.Independence.Basic (iIndepFun_pi). Candes-Recht 2009 arXiv:0805.4471 section 6 (independent Bernoulli sampling).

View graph