The real Gaussian probit: Φ, Φ⁻¹, and the Cohen radius as a THEOREM #
The complete G1–G4 ladder of planning/archive/smoothing_gaussian_lemma.md. Endpoint:
smoothing_certified_radius_classifier — for a measurable classifier under N(0,σ²I)
smoothing, every ‖δ‖ < σ·Φ⁻¹(p_A(x)) provably cannot flip the smoothed argmax, with
Φ⁻¹ the genuine standard-normal quantile and NO smoothing-side hypotheses left: the
Cohen–Rosenfeld–Kolter (1/σ)-Lipschitz probit (hg of the G1 radius theorem, the
Neyman–Pearson hard half) is now smoothing_probit_lipschitz, a theorem.
stdNormalCDF is Mathlib's cdf (gaussianReal 0 1) — the genuine Φ, no bespoke integral.
This file proves the three facts Mathlib doesn't have:
- strict monotonicity (
stdNormalCDF_strictMono) — the Gaussian pdf is everywhere positive, so every interval carries positive mass; - symmetry
Φ(−t) = 1 − Φ(t)(stdNormalCDF_neg) — the standard Gaussian is invariant under negation (gaussianReal_map_neg); - the quantile
stdNormalQuantile p = sSup {t | Φ t < p}is monotone on(0,1)(stdNormalQuantile_monotoneOn) and odd about ½ (stdNormalQuantile_anti,Φ⁻¹(1−q) = −Φ⁻¹(q)), via the no-flat-step lemmastdNormalCDF_sSup_lt_eq_sInf_gt(a flat step at levelqwould give two points withΦ = q, against strict mono).
The two-sided inverse is fully packaged: Φ(Φ⁻¹ p) = p on (0,1)
(stdNormalCDF_quantile), Φ⁻¹(Φ s) = s globally (stdNormalQuantile_cdf), and from
those Φ⁻¹ is strictly monotone on (0,1) (stdNormalQuantile_strictMonoOn), maps
(0,1) onto ℝ (stdNormalQuantile_surjOn), and is continuous there
(stdNormalQuantile_continuousAt/_continuousOn — strict mono + full image, no extra
measure theory).
G2 (the 1-D Neyman–Pearson core) also lives here: stdNormalCDF_quantile upgrades the
quantile to a genuine inverse (Φ(Φ⁻¹ p) = p on (0,1), right-continuity + no-atoms), and
gaussian_np_shift is the Cohen bound — a [0,1] function with N(0,1)-mean ≥ Φ(t) keeps
mean ≥ Φ(t−δ) under a δ ≥ 0 shift, by the monotone-likelihood-ratio pointwise inequality
(f − 1_{z≤t})·(LR − LR(t)) ≥ 0 (no layer-cake, no rearrangement machinery).
Capstone: smoothing_certified_radius_gaussian — smoothing_certified_radius_probit with
Phiinv := stdNormalQuantile, its hmono/hanti DISCHARGED. The quantile is total on ℝ
(junk sSup outside (0,1)) but every use here is guarded by hp : p c y ∈ Ioo 0 1 — the
realistic regime, since Monte-Carlo/Clopper–Pearson class-probability estimates are never
exactly 0 or 1. See planning/archive/smoothing_gaussian_lemma.md for why the ORIGINAL abstract
theorem's global Monotone Phiinv can never be met by the true (unbounded) quantile.
All results are propext / Classical.choice / Quot.sound-clean (tests/AuditAxioms.lean).
The standard-normal CDF Φ — Mathlib's cdf of the genuine gaussianReal 0 1.
Equations
Instances For
The standard-normal quantile Φ⁻¹, as sSup {t | Φ t < p}. Total on ℝ (junk value
outside (0,1), where the defining set is empty or unbounded); the honest inverse on
(0,1), which is where every guarded use below lives.
Equations
- Proofs.stdNormalQuantile p = sSup {t : ℝ | Proofs.stdNormalCDF t < p}
Instances For
Every open interval carries positive standard-Gaussian mass (the pdf is everywhere positive). The engine of strict monotonicity.
Φ is strictly monotone: Φ t − Φ s = P(Ioc s t) > 0 for s < t.
Gaussian symmetry Φ(−t) = 1 − Φ(t): the standard Gaussian is invariant under
negation, so P(Iic (−t)) = P(Ici t), and (no atoms) the complement gives the rest.
Φ → 0 at −∞, so for p > 0 some t has Φ t < p — the quantile's set is
nonempty.
Φ → 1 at +∞, so for p < 1 some t has Φ t > p.
hmono discharged: the real quantile is monotone on (0,1) — larger p, larger
sub-level set, larger sSup.
No flat step at level q: sSup {Φ < q} = sInf {Φ > q}. Any gap between them
would contain two points where Φ = q exactly — impossible for a strictly monotone
Φ. The bridge between the quantile's sSup form and its mirrored sInf form.
hanti discharged: the real quantile is odd about ½, Φ⁻¹(1−q) = −Φ⁻¹(q) on
(0,1). Symmetry turns {Φ < 1−q} into the negation of {Φ > q}, sSup ∘ neg
into −sInf, and the no-flat-step lemma closes the sInf/sSup mismatch.
The quantile genuinely inverts Φ on (0,1): Φ(Φ⁻¹ p) = p. Right continuity of
the Stieltjes cdf gives ≥ (a value below p at the sup would push the sup further
right); no-atoms gives ≤ (the cdf equals its left limit, and everything left of the
sup is < p). The lemma that makes stdNormalQuantile an inverse, not just a
monotone-odd stand-in — G2's Neyman–Pearson bound enters through it.
The analytic heart of Cohen 2019, in its 1-D normalized form. The classic proof needs
no layer-cake and no rearrangement machinery: with h the halfspace indicator at the
threshold t and LR the (monotone) Gaussian likelihood ratio, the pointwise inequality
(f − h)·(LR − LR(t)) ≥ 0 — sign-checked on each side of t — integrates against the
base Gaussian into exactly the Neyman–Pearson optimality of the halfspace.
The Gaussian likelihood ratio: pdf_{N(δ,1)}(z) = exp(δz − δ²/2) · pdf_{N(0,1)}(z) —
monotone in z (for δ ≥ 0), which is all Neyman–Pearson needs.
The shifted Gaussian's cdf is a shifted Φ: cdf_{N(δ,1)}(t) = Φ(t − δ).
The halfspace indicator's Gaussian mass is the cdf at the threshold.
G2 — the 1-D Neyman–Pearson core (Cohen 2019, Lemma 3 specialization). For
measurable f : ℝ → [0,1] with standard-Gaussian mean at least Φ(t), the mean under
the δ-shifted Gaussian (δ ≥ 0) is at least Φ(t − δ): among all [0,1] functions
of given Gaussian mass, the halfspace indicator 1_{z ≤ t} loses the most mass under a
shift — the likelihood ratio exp(δz − δ²/2) is monotone, so
(f − 1_{z ≤ t})·(LR − LR(t)) ≥ 0 pointwise, and integrating it against N(0,1)
forces ∫f dN(δ,1) ≥ ∫1_{z ≤ t} dN(δ,1) = Φ(t − δ).
Randomized-smoothing certified radius at the true Gaussian probit. With class
probabilities honestly inside (0,1) (hp), per-class probit scores
Φ⁻¹ ∘ p c each (1/σ)-Lipschitz (hg — the Neyman–Pearson core, the ONE remaining
smoothing-side hypothesis, G2–G4 of planning/archive/smoothing_gaussian_lemma.md), and the
runner-up bound, every ‖δ‖₂ < σ·Φ⁻¹(p_A(x)) keeps class i the strict argmax —
where Φ⁻¹ is now the genuine standard-normal quantile, not an abstract stand-in.
Exactly the σ·Φ⁻¹(p_A) radius the *-smooth drivers report.
The n-D Cohen bound ∫f(·+δ) dγ ≥ Φ(Φ⁻¹(∫f dγ) − ‖δ‖) for the standard Gaussian γ
on EuclideanSpace ℝ (Fin (n+1)). Structure: (i) a 1-D Cameron–Martin change of variables
turns the shifted integral into a monotone-likelihood-ratio-weighted one; (ii) Fubini over
Measure.pi (split at coordinate 0 via piFinSuccAbove) lifts it to the iid pi measure —
only coordinate 0 carries the shift; (iii) the same pointwise MLR trick as G2, now with the
weight exp(d·z₀ − d²/2) and the halfspace {z₀ ≤ t}, gives the pi-space NP theorem;
(iv) an adapted orthonormal basis (a reflection carries e₀ to δ/‖δ‖, and Mathlib's
stdGaussian_eq_map_pi_orthonormalBasis says the standard Gaussian doesn't care) rotates
the general shift onto coordinate 0. The plan's riskiest item — pi-Gaussian rotational
invariance — turned out to ship with Mathlib.
The iid standard-Gaussian product measure on Fin (n+1) → ℝ.
Equations
- Proofs.stdGaussianPi n = MeasureTheory.Measure.pi fun (x : Fin (n + 1)) => ProbabilityTheory.gaussianReal 0 1
Instances For
The exponential weight is Gaussian-integrable.
Assembly. stdNormalQuantile_cdf (the other inversion direction, Φ⁻¹(Φ s) = s, from
strict monotonicity) plus stdNormalCDF_mem_Ioo let the G3 bound be pushed through Φ⁻¹:
applying it in both directions gives |Φ⁻¹(p(x)) − Φ⁻¹(p(y))| ≤ ‖x−y‖/σ — the Cohen/Salman
(1/σ)-Lipschitz probit, smoothing_probit_lipschitz. Instantiating the G1 radius theorem
with it yields smoothing_certified_radius_cohen (soft scores) and
smoothing_certified_radius_classifier (hard classifier — the [0,1] bounds AND the
runner-up bound come free from decision-region disjointness). The σ-smoothed mean is
written ∫ f(x + σ•z) dγ(z) with γ the STANDARD Gaussian — i.e. noise N(0, σ²I),
exactly what the *-smooth drivers sample.
Φ⁻¹(Φ s) = s — the quantile inverts the cdf everywhere (strict monotonicity makes
the strict sub-level set of Φ s exactly Iio s).
Φ never reaches 0: there is Gaussian mass below every point.
Φ never reaches 1 (symmetry + stdNormalCDF_pos).
Φ maps into the open unit interval.
Φ⁻¹ is STRICTLY monotone on (0,1) (upgrade of stdNormalQuantile_monotoneOn):
reflect strictness through Φ via the two-sided inverse stdNormalCDF_quantile.
Φ⁻¹ maps (0,1) ONTO ℝ: every real s is Φ⁻¹(Φ s).
Φ⁻¹ is continuous at every p ∈ (0,1): strictly monotone on the open interval
with image all of ℝ (a neighborhood of anything).
Φ⁻¹ is continuous on (0,1).
G4 core — the smoothed probit is (1/σ)-Lipschitz (Cohen 2019 / Salman 2019
Lemma 2, now a THEOREM). For measurable f : E → [0,1] whose σ-smoothed mean
p(x) = ∫ f(x + σz) dγ(z) stays inside (0,1), the probit score
x ↦ Φ⁻¹(p x) is (1/σ)-Lipschitz in L2.
The Cohen radius, Neyman–Pearson side DISCHARGED. For a family of measurable
[0,1] class scores whose σ-smoothed means stay in (0,1), the smoothed prediction
cannot flip within ‖δ‖ < σ·Φ⁻¹(p_i(x)). No Lipschitz hypothesis: hg is now the
theorem smoothing_probit_lipschitz.
The classifier form. For a measurable hard classifier C, class scores are the
decision-region indicators, so [0,1]-boundedness AND the runner-up bound are both
automatic (regions are disjoint: p_j + p_i ≤ 1). Hypotheses: measurability of C,
non-degenerate class probabilities (hp — Φ⁻¹ needs (0,1); Monte-Carlo estimates
always satisfy this), and the margin ‖δ‖ < σ·Φ⁻¹(p_i(x)). This is the certificate
the *-smooth drivers report, end to end.