bernoulli_event_prob_nonneg

Proved

by Minghui · Jun 24, 2026 · Mathlib c5ea003 (Lean v4.30.0)

bernoulli-modelcandes-rechtformal-bridgematrix-completionprobability

Source: Candes--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 18, Section 4.1, equations (4.3)--(4.4), where the paper introduces the Bernoulli observation model with independent coordinate indicators.

Mathematical statement: for an $n_1 \times n_2$ matrix index set and Bernoulli inclusion parameter $p$ , define $\Omega \subseteq [n_1]\times[n_2]$ with mass

w_p(\Omega)=p^{|\Omega|}(1-p)^{n_1n_2-|\Omega|}.

If $0\le p\le 1$ , then every event $E$ has nonnegative Bernoulli event probability

\mathbb P_p(E)=\sum_\Omega \mathbf 1_E(\Omega) w_p(\Omega) \ge 0.

Notation: here $p$ is the Bernoulli sampling rate from Candes--Recht Section 4.1, $\Omega$ is a finite sampled entry set, and bernoulliEventProb p Event is the formal finite sum over all $\Omega$ .

Formalization note: this is a formal bridge, not a new analytic concentration theorem and not a theorem that appears verbatim in the paper. It is a reusable probability-mass sanity lemma for source-backed Bernoulli-model children, whose source-backed parent context is the Bernoulli model in Candes--Recht PDF p. 18, Section 4.1, equations (4.3)--(4.4).

Preamble

import Definitions.Def_matrix_completion_bernoulli

open MatrixCompletion
open scoped Classical BigOperators

Formal statement

theorem bernoulli_event_prob_nonneg
    {n₁ n₂ : ℕ} {p : ℝ}
    (Event : Finset (Fin n₁ × Fin n₂) → Prop) :
    0 ≤ p → p ≤ 1 → 0 ≤ bernoulliEventProb p Event := by
  sorry

Source

Candes--Recht, Exact Matrix Completion via Convex Optimization, PDF p. 18, Section 4.1, equations (4.3)--(4.4); formal bridge for the Bernoulli probability mass used by source-backed Bernoulli-model children.

View graph