bernoulli_finite_index_intersection_probability_from_pointwise_bounds

Proved

by Shuze Chen · Jun 21, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bernoulli-samplingcandes-rechtfinite-indexlean4matrix-completionunion-bound

Finite-index Bernoulli union bound with the index-cardinality loss explicit.

Let $\iota$ be any finite index type. For each $i\in\iota$ , let $E_i(\Omega)$ be an event in the Bernoulli observation model with parameter $p\in[0,1]$ . If

\mathbb P_p(E_i)\ge 1-c\eta\qquad\text{for every }i\in\iota,

then

\mathbb P_p\{\forall i\in\iota,\ E_i\} \ge 1-|\iota|c\eta.

This is the reusable finite-union-bound primitive for coordinate and pair-coordinate uniformization. The cardinality factor is deliberately visible; later scalar estimates must absorb it explicitly.

Source context: standard finite union bound, used throughout the coefficient-uniformization arguments in Candes-Recht 2008, Section 6.

Preamble

import Definitions.Def_matrix_completion_bernoulli
open MatrixCompletion
universe u

Formal statement

theorem bernoulli_finite_index_intersection_probability_from_pointwise_bounds
    {ι : Type u} [Fintype ι] [DecidableEq ι] {n₁ n₂ : ℕ}
    (p c failureScale : ℝ)
    (Event : ι → Finset (Fin n₁ × Fin n₂) → Prop) :
    0 ≤ p → p ≤ 1 →
    (∀ i : ι, bernoulliEventProb p (Event i) ≥ 1 - c * failureScale) →
    bernoulliEventProb p (fun Omega => ∀ i : ι, Event i Omega) ≥
      1 - (((Fintype.card ι : ℝ) * c) * failureScale) := by
  sorry

Source

Candes, Emmanuel, and Benjamin Recht. "Exact matrix completion via convex optimization." Communications of the ACM 55.6 (2012): 111-119.

View graph