dlp_eq7_pair_integration

Proved

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

de la Peña–Montgomery-Smith 1995 (arXiv:math/9309211) §4 eq (7) integration combinator on the finite Bernoulli pair model. If on each pair-fiber (Ω₁,Ω₂) the event Good Ω₁ Ω₂ forces condBound Ω₁ Ω₂ ≥ c for a constant c ≥ 0, then summing against the nonnegative bernoulli pair weights gives c · bernoulliPairEventProb p Good ≤ bernoulliPairExpectation p condBound. This is the measure-free 'integrate over {‖T_{n,k}‖ ≥ t}' step (eq 6 → eq 7, p.5).

Preamble

import Definitions.Def_matrix_completion_bernoulli
import Definitions.Def_matrix_completion_neumann
open MatrixCompletion
open scoped BigOperators Classical

Formal statement

theorem dlp_eq7_pair_integration
    {n1 n2 : Nat} (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
    (c : ℝ) (hc : 0 ≤ c)
    (condBound : Finset (Fin n1 × Fin n2) → Finset (Fin n1 × Fin n2) → ℝ)
    (Good : Finset (Fin n1 × Fin n2) → Finset (Fin n1 × Fin n2) → Prop)
    (hcond_nonneg : ∀ Ω₁ Ω₂, 0 ≤ condBound Ω₁ Ω₂)
    (hfiber : ∀ Ω₁ Ω₂, Good Ω₁ Ω₂ → c ≤ condBound Ω₁ Ω₂) :
    c * bernoulliPairEventProb p Good ≤ bernoulliPairExpectation p condBound := by
  sorry

View graph