The real Gaussian probit: Φ, Φ⁻¹, and the Cohen radius as a THEOREM #

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. The Cohen–Rosenfeld–Kolter (1/σ)-Lipschitz probit (hg of smoothing_certified_radius_probit, the Neyman–Pearson half) is a theorem here, smoothing_probit_lipschitz. The one remaining hypothesis on the smoothed classifier is hp: every class's smoothed probability lies in (0,1) at every point. Smoothing.NetSemantics discharges it for argmax nets.

Φ (stdNormalCDF, Mathlib's cdf (gaussianReal 0 1)), Φ⁻¹ (stdNormalQuantile) and their monotonicity, symmetry, two-sided inversion and continuity live in GaussianQuantile.lean. This file proves:

• the Neyman–Pearson bounds: pi_gaussian_np_shift — a [0,1] function with mean ≥ Φ(t) under the iid product stdGaussianPi n keeps mean ≥ Φ(t−d) under a d ≥ 0 shift along coordinate 0, by the monotone-likelihood-ratio pointwise inequality (F − 1_{z₀≤t})·(LR − LR(t)) ≥ 0 (no layer-cake, no rearrangement machinery) — and its rotation to an arbitrary shift on Euclidean space, stdGaussian_np_shift;
• the (1/σ)-Lipschitz probit, smoothing_probit_lipschitz;
• the Cohen radius at the real quantile: smoothing_certified_radius_gaussian (abstract scores, hg still a hypothesis), smoothing_certified_radius_cohen (Gaussian-smoothed [0,1] scores), smoothing_certified_radius_classifier (hard classifier), and smoothing_certified_of_le (any lower bound on the top-class probability certifies).

The quantile is total on ℝ (junk sSup outside (0,1)), and every use here is guarded by hp. smoothing_certified_radius_probit asks monotonicity of the probit only on (0,1) because no globally monotone function agrees with the true (unbounded) quantile there.

All results are propext / Classical.choice / Quot.sound-clean (tests/AuditAxioms.lean).

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 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 the 1-D case, 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.

Assembly. stdNormalQuantile_cdf (the other inversion direction, Φ⁻¹(Φ s) = s, from strict monotonicity) plus stdNormalCDF_mem_Ioo let the n-D bound stdGaussian_np_shift 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 smoothing_certified_radius_gaussian 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.