The Monte-Carlo tie for randomized smoothing #
smoothing_certified_radius_classifier (SmoothingGaussian.lean) certifies the
radius σ·Φ⁻¹(p) for the TRUE class probability p = ∫ 1[C(x+σz)=y] dγ(z).
The *-smooth drivers can only ESTIMATE p from N Gaussian samples — the
honest gap flagged since the smoothing theorems landed.
This file closes it: a one-sided Hoeffding bound for [0,1]-valued
Monte-Carlo means over the product measure (mc_mean_lower_bound, built on
Mathlib's HasSubgaussianMGF machinery), so that with probability
≥ 1 − exp(−2Nt²) over the samples, the true p is at least the empirical
p̂ − t — and on that event the reported radius σ·Φ⁻¹(p̂ − t) is genuinely
certified (smoothing_mc_certified, composed with the classifier theorem
through the quantile's monotonicity). The guarantee has exactly the shape of
Cohen et al.'s CERTIFY procedure: a confidence-qualified radius, now end to
end a theorem.
One-sided Hoeffding for a [0,1]-valued Monte-Carlo mean. With
probability ≥ 1 − exp(−2Nt²) over N iid samples from ν, the
empirical mean minus t lower-bounds the true mean.
Below 0 the quantile's defining set is empty (Φ > 0 everywhere), so
Φ⁻¹ takes the junk value sSup ∅ = 0 — and the radius σ·Φ⁻¹(p̂−t)
certifies vacuously.
The Monte-Carlo smoothing certificate. Sample N iid standard
Gaussians; report the radius σ·Φ⁻¹(p̂ − t) from the empirical class
frequency p̂. With probability ≥ 1 − exp(−2Nt²) over the samples, the
reported radius is GENUINELY certified: every ‖δ‖ < σ·Φ⁻¹(p̂ − t) keeps
y the strict argmax of the smoothed classifier. This is the guarantee
shape of Cohen–Rosenfeld–Kolter's CERTIFY procedure, with the Neyman–
Pearson side (smoothing_probit_lipschitz), the radius algebra
(smoothing_certified_radius_classifier), and now the sampling
confidence (mc_mean_lower_bound, Hoeffding) all theorems.