Candès–Romberg Talagrand theorem on a finite Boolean product space

Proved

TalagrandCore.candes_romberg_talagrand_leaf

by Harry_Xu · Aug 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

concentration-inequalitiesempirical-processesprobabilitytalagrand

For every finite centered Bernoulli linear class with coefficient envelope $B>0$ and variance proxy $\sigma^2$ , there is a universal constant $K>0$ such that, for all $t\ge0$ ,

\mathbb P\{|Z-\mathbb EZ|>t\} \le 3\exp\!\left(-\frac{t}{KB}\log\left(1+\frac{Bt}{\sigma^2+B\mathbb E\bar Z}\right)\right).

This is the finite Boolean product-measure form of Candès–Romberg Theorem 3.2, obtained from the unit-envelope result by scaling and then bridged from finite weighted sums to the product-measure integral.

Formalization Note The theorem uses an existential universal constant; the extracted proof supplies the explicit value $K=57600$ .

Preamble

import Definitions.Def_talagrand_finite_bool_core
open MeasureTheory
open scoped Classical BigOperators

Formal statement

namespace TalagrandCore

variable {κ ι : Type} [DecidableEq κ] [Fintype κ]
variable [Fintype ι] [Nonempty ι]

theorem candes_romberg_talagrand_leaf :
    ∃ K : ℝ, 0 < K ∧
      ∀ (κ : Type) [Fintype κ] (p : NNReal) (hp : p ≤ 1)
        (ι : Type) [Fintype ι] [Nonempty ι]
        (coeff : ι → κ → ℝ) (B sigmaSq t : ℝ),
        0 < B → 0 ≤ sigmaSq → 0 ≤ t →
        (∀ a : ι, ∀ x : κ, |coeff a x| ≤ B) →
        (∀ a : ι,
          ∑ x : κ, (p : ℝ) * (1 - (p : ℝ)) * (coeff a x) ^ 2 ≤ sigmaSq) →
        let boolProcess : ι → (κ → Bool) → ℝ :=
          fun a ω =>
            ∑ x : κ, ((cond (ω x) (1 : ℝ) 0 - (p : ℝ)) * coeff a x)
        let boolZ : (κ → Bool) → ℝ :=
          fun ω => Finset.univ.sup' Finset.univ_nonempty
            (fun a : ι => boolProcess a ω)
        let boolZbar : (κ → Bool) → ℝ :=
          fun ω => Finset.univ.sup' Finset.univ_nonempty
            (fun a : ι => |boolProcess a ω|)
        (Measure.pi (fun _ : κ => (PMF.bernoulli p hp).toMeasure)).real
            {ω | ¬ |boolZ ω -
                  (∫ ω, boolZ ω
                    ∂(Measure.pi (fun _ : κ => (PMF.bernoulli p hp).toMeasure)))| ≤ t} ≤
          3 * Real.exp
            (-(t / (K * B)) *
              Real.log
                (1 + (B * t) /
                  (sigmaSq + B *
                    (∫ ω, boolZbar ω
                      ∂(Measure.pi (fun _ : κ => (PMF.bernoulli p hp).toMeasure)))))) := by sorry

end TalagrandCore

Source

Emmanuel Candès and Justin Romberg, Sparsity and Incoherence in Compressive Sampling, Section 3, Theorem 3.2 and equation (3.9), PDF p. 12. Formal Lean proof extracted from Prove2Me accepted submission bf106d23-ff42-48f5-a837-a8528101c849 by tianyipeng.

View graph