Documentation

LeanMlir.Proofs.Certificates.SmoothingCP

The exact Clopper–Pearson tie for randomized smoothing #

smoothing_mc_certified (SmoothingMC.lean) qualifies the reported radius with Hoeffding's 1 − exp(−2Nt²) — a crude bound. Cohen–Rosenfeld–Kolter's CERTIFY actually deploys the EXACT binomial lower confidence limit (Clopper–Pearson, proportion_confint one-sided). This file closes that last arithmetic gap:

pi_hitCount_eq_binomial — the count of successes over Measure.pi is binomial (the piece Mathlib doesn't have: Bin(n,p) exists as setBer(Iio n, p).map ncard, but no law-of-the-iid-indicator-count): induction on N through measurePreserving_piFinSuccAbove, splitting the first coordinate by Fubini and closing with Pascal's rule;
cpLower α N k = sInf {q ∈ [0,1] | α < binomTail N k q} — the CP lower bound, with binomTail the literal tail polynomial the driver evaluates;
cp_coverage — with probability ≥ 1 − α the CP bound is a genuine lower bound for the true probability. The sInf definition makes coverage need NO tail-monotonicity in q: the minimal counterexample count k₀ has p < cpLower α N k₀, so binomTail N k₀ p ≤ α directly (contrapositive of csInf_le), and every count below k₀ certifies by minimality of k₀;
smoothing_cp_certified — composed with smoothing_certified_radius_classifier: with probability ≥ 1 − α over the N Gaussian samples, the radius σ·Φ⁻¹(cpLower α N k) reported from the observed class count k is genuinely certified. Guarantee AND arithmetic now match the deployed CERTIFY;
the SOLVED form (the per-image scorecard shape): binomTail_monotoneOn — monotone in the success probability by COUPLING (uniform measure on [0,1], nested [0,q] ⊆ [0,p], tail events nest — the tail law again, no calculus) — gives le_cpLower_of_tail_le: ONE kernel tail check binomTail N k₀ q₀ ≤ α certifies the driver's reported q₀, and smoothing_cp_certified_solved turns it into "if the count comes out k₀, the radius σ·Φ⁻¹(q₀) is certified" (w.p. ≥ 1 − α);
the KERNEL ENGINE (the ListDot recipe): binomTailNum — a kernel- computable ℕ tail numerator (descFactorial/factorial binomials on the small side) — with the once-proven bridge binomTail_eq_kernel, so each per-image hypothesis is ONE decide +kernel bignum inequality (binomTail_le_of_kernel_check), as SmoothingCPScorecard.lean states them.

All results are propext / Classical.choice / Quot.sound-clean.

noncomputable def Proofs.binomTail (N k : ℕ) (q : ℝ) :

Upper tail of the Binomial(N, q) distribution: P(X ≥ k) as a real polynomial in q — exactly what the driver evaluates.

Equations

Proofs.binomTail N k q = ∑ j ∈ Finset.Icc k N, ↑(N.choose j) * q ^ j * (1 - q) ^ (N - j)

Instances For

noncomputable def Proofs.cpLower (α : ℝ) (N k : ℕ) :

The Clopper–Pearson lower confidence bound at level α for k successes in N trials: the smallest success probability whose upper tail at k still exceeds α.

Equations

Proofs.cpLower α N k = sInf {q : ℝ | q ∈ Set.Icc 0 1 ∧ α < Proofs.binomTail N k q}

Instances For

theorem Proofs.binomTail_le_of_lt_cpLower {α p : ℝ} (hp : p ∈ Set.Icc 0 1) {N k : ℕ} (h : p < cpLower α N k) :

binomTail N k p ≤ α

The CP key inequality: if the true p lies strictly below the CP lower bound, its tail is at most α (contrapositive of sInf ≤).

noncomputable def Proofs.hitCount {E : Type u_1} (A : Set E) (N : ℕ) (ω : Fin N → E) :

The number of samples landing in A, as a Fin N-indexed indicator sum (Set.indicator: no decidability needed).

Equations

Proofs.hitCount A N ω = ∑ i : Fin N, A.indicator 1 (ω i)

Instances For

theorem Proofs.hitCount_mono {E : Type u_1} {A B : Set E} (hAB : A ⊆ B) (N : ℕ) (ω : Fin N → E) :

hitCount A N ω ≤ hitCount B N ω

The count is monotone in the target set.

theorem Proofs.hitCount_le {E : Type u_1} (A : Set E) (N : ℕ) (ω : Fin N → E) :

hitCount A N ω ≤ N

theorem Proofs.measurable_hitCount {E : Type u_1} [MeasurableSpace E] {A : Set E} (hA : MeasurableSet A) (N : ℕ) :

Measurable (hitCount A N)

theorem Proofs.hitCount_insertNth_zero {E : Type u_1} (A : Set E) (N : ℕ) (x : E) (τ : Fin N → E) :

hitCount A (N + 1) (Fin.insertNth 0 x τ) = A.indicator 1 x + hitCount A N τ

Prepending a sample to the tuple adds its indicator to the count.

theorem Proofs.pi_hitCount_eq_binomial {E : Type u_1} [MeasurableSpace E] (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] {A : Set E} (hA : MeasurableSet A) (N j : ℕ) :

(MeasureTheory.Measure.pi fun (x : Fin N) => ν) {ω : Fin N → E | hitCount A N ω = j} = ↑(N.choose j) * ν A ^ j * ν Aᶜ ^ (N - j)

The count of successes over the product measure is binomial (point law, ℝ≥0∞ form): P(hitCount = j) = C(N,j)·ν(A)^j·ν(Aᶜ)^(N−j). Induction on N through the coordinate-0 product split, Fubini on the first sample, and Pascal's rule.

theorem Proofs.pi_hitCount_real_eq_binomial {E : Type u_1} [MeasurableSpace E] (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] {A : Set E} (hA : MeasurableSet A) (N j : ℕ) :

(MeasureTheory.Measure.pi fun (x : Fin N) => ν).real {ω : Fin N → E | hitCount A N ω = j} = ↑(N.choose j) * ν.real A ^ j * (1 - ν.real A) ^ (N - j)

The point law in real form.

theorem Proofs.pi_hitCount_tail_real {E : Type u_1} [MeasurableSpace E] (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] {A : Set E} (hA : MeasurableSet A) (N k : ℕ) :

(MeasureTheory.Measure.pi fun (x : Fin N) => ν).real {ω : Fin N → E | k ≤ hitCount A N ω} = binomTail N k (ν.real A)

The upper-tail law: P(hitCount ≥ k) over the product measure is exactly the binomTail polynomial the CP bound is defined from.

theorem Proofs.cp_coverage {E : Type u_1} [MeasurableSpace E] (ν : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure ν] {A : Set E} (hA : MeasurableSet A) (N : ℕ) {α : ℝ} (hα : 0 ≤ α) :

1 - α ≤ (MeasureTheory.Measure.pi fun (x : Fin N) => ν).real {ω : Fin N → E | cpLower α N (hitCount A N ω) ≤ ν.real A}

Clopper–Pearson coverage. With probability at least 1 − α over the N iid samples, the CP lower bound computed from the observed count is a genuine lower bound for the true probability ν(A). No tail-monotonicity in the parameter is needed: the minimal-counterexample count k₀ has p < cpLower α N k₀, so its tail at p is ≤ α by the sInf defining property, and every count below k₀ certifies by minimality.

theorem Proofs.binomTail_monotoneOn (N k : ℕ) :

MonotoneOn (binomTail N k) (Set.Icc 0 1)

The binomial tail is monotone in the success probability — by COUPLING, not calculus: instantiate the tail law at the uniform measure on [0,1] with the nested sets [0,q] ⊆ [0,p], and the tail events nest pointwise.

theorem Proofs.binomTail_one {N k : ℕ} (hk : k ≤ N) :

binomTail N k 1 = 1

At q = 1 the tail is exactly 1 (only the j = N term survives).

theorem Proofs.le_cpLower_of_tail_le {α q₀ : ℝ} (hα : α < 1) {N k : ℕ} (hk : k ≤ N) (hq₀ : q₀ ∈ Set.Icc 0 1) (h : binomTail N k q₀ ≤ α) :

q₀ ≤ cpLower α N k

The solved-form CP bound: one in-kernel tail check binomTail N k q₀ ≤ α certifies q₀ as a lower bound for cpLower — the form the driver's reported q₀ can be verified in.

theorem Proofs.smoothing_cp_certified {n k : ℕ} {σ : ℝ} (hσ : 0 < σ) {C : EuclideanSpace ℝ (Fin (n + 1)) → Fin k} (hC : Measurable C) (hp : ∀ (c : Fin k) (x : EuclideanSpace ℝ (Fin (n + 1))), ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if C (x + σ • z) = c then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1))) ∈ Set.Ioo 0 1) (x : EuclideanSpace ℝ (Fin (n + 1))) (y : Fin k) (N : ℕ) {α : ℝ} (hα : 0 ≤ α) :

1 - α ≤ (MeasureTheory.Measure.pi fun (x : Fin N) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1)))).real {ω : Fin N → EuclideanSpace ℝ (Fin (n + 1)) | ∀ (δ : EuclideanSpace ℝ (Fin (n + 1))), ‖δ‖ < σ * stdNormalQuantile (cpLower α N (∑ i : Fin N, if C (x + σ • ω i) = y then 1 else 0)) → ∀ (j : Fin k), j ≠ y → ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if C (x + δ + σ • z) = j then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1))) < ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if C (x + δ + σ • z) = y then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1)))}

The Clopper–Pearson smoothing certificate. Sample N iid standard Gaussians; report the radius σ·Φ⁻¹(cpLower α N k) from the exact binomial lower confidence limit at the observed class count k. With probability ≥ 1 − α over the samples, the reported radius is GENUINELY certified: every ‖δ‖ < σ·Φ⁻¹(cpLower α N k) keeps y the strict argmax of the smoothed classifier. Same guarantee shape as smoothing_mc_certified, but the confidence bound is now the arithmetic Cohen's CERTIFY actually deploys.

theorem Proofs.smoothing_cp_certified_solved {n k : ℕ} {σ : ℝ} (hσ : 0 < σ) {C : EuclideanSpace ℝ (Fin (n + 1)) → Fin k} (hC : Measurable C) (hp : ∀ (c : Fin k) (x : EuclideanSpace ℝ (Fin (n + 1))), ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if C (x + σ • z) = c then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1))) ∈ Set.Ioo 0 1) (x : EuclideanSpace ℝ (Fin (n + 1))) (y : Fin k) {N k₀ : ℕ} (hk₀ : k₀ ≤ N) {α q₀ : ℝ} (hα : 0 ≤ α) (hα1 : α < 1) (hq₀ : q₀ ∈ Set.Ioo 0 1) (htail : binomTail N k₀ q₀ ≤ α) :

1 - α ≤ (MeasureTheory.Measure.pi fun (x : Fin N) => ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1)))).real {ω : Fin N → EuclideanSpace ℝ (Fin (n + 1)) | (∑ i : Fin N, if C (x + σ • ω i) = y then 1 else 0) = k₀ → ∀ (δ : EuclideanSpace ℝ (Fin (n + 1))), ‖δ‖ < σ * stdNormalQuantile q₀ → ∀ (j : Fin k), j ≠ y → ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if C (x + δ + σ • z) = j then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1))) < ∫ (z : EuclideanSpace ℝ (Fin (n + 1))), if C (x + δ + σ • z) = y then 1 else 0 ∂ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin (n + 1)))}

The driver tie, solved form. For the OBSERVED count k₀ and the driver's reported CP lower bound q₀ (rationalized down), ONE in-kernel tail check binomTail N k₀ q₀ ≤ α certifies: with probability ≥ 1 − α over the samples, IF the count comes out k₀ THEN the radius σ·Φ⁻¹(q₀) is genuinely certified. This is the per-image scorecard theorem shape: instantiate at the driver's (N, k₀, α, q₀) and the hypothesis is pure kernel rational arithmetic.

Summing the tail term by term with norm_num prices out at driver scale (N = 10112, hundreds of terms, Nat.choose far from the diagonal). The ListDot recipe applies instead: a kernel-computable ℕ numerator + a once-proven bridge, so each per-image scorecard hypothesis is ONE decide +kernel bignum inequality (~0.1 s even for thousands of terms — kernel Nat.pow/mul are GMP-accelerated).

def Proofs.binomTailNum (N k a d : ℕ) :

Kernel-computable tail numerator: Σ_{i=0}^{N-k} C(N,i)·a^(N-i)·(d-a)^i (i = N - j, so the binomial coefficient rides the SMALL side, and descFactorial/factorial computes it free of the exponential Pascal recursion — Nat.choose_eq_descFactorial_div_factorial makes the truncated division exact).

Equations

Proofs.binomTailNum N k a d = ∑ i ∈ Finset.range (N - k + 1), N.descFactorial i / i.factorial * a ^ (N - i) * (d - a) ^ i

Instances For

theorem Proofs.binomTailNum_eq {N k : ℕ} (hk : k ≤ N) (a d : ℕ) :

binomTailNum N k a d = ∑ j ∈ Finset.Icc k N, N.choose j * a ^ j * (d - a) ^ (N - j)

The kernel numerator is the tail's numerator over Icc k N (reflect the range, Nat.choose_symm).

theorem Proofs.binomTail_eq_kernel {N k : ℕ} (hk : k ≤ N) {a d : ℕ} (ha : a ≤ d) (hd : 0 < d) :

binomTail N k (↑a / ↑d) = ↑(binomTailNum N k a d) / ↑d ^ N

The real tail at a rational a/d equals the kernel numerator over d^N.

theorem Proofs.binomTail_le_of_kernel_check {N k a d A : ℕ} (hk : k ≤ N) (ha : a ≤ d) (hd : 0 < d) (hA : 0 < A) (hcheck : A * binomTailNum N k a d ≤ d ^ N) :

binomTail N k (↑a / ↑d) ≤ 1 / ↑A

One kernel bignum inequality certifies a tail bound: the per-image scorecard hypothesis at q₀ = a/d, α = 1/A, discharged by decide +kernel.