The standard normal: Φ, its quantile Φ⁻¹, and full support #
stdNormalCDF (Mathlib's cdf of gaussianReal 0 1) and stdNormalQuantile (sSup {t | Φ t < p},
the honest inverse on (0,1)), with the facts every smoothing certificate uses: Φ is strictly
monotone and symmetric; on (0,1) the quantile is strictly monotone (stdNormalQuantile_strictMonoOn),
odd about ½, continuous (stdNormalQuantile_continuousAt, stdNormalQuantile_continuousOn) and
inverts Φ both ways (stdNormalCDF_quantile, stdNormalQuantile_cdf; onto ℝ,
stdNormalQuantile_surjOn); below 0 it takes the junk value 0. Mathlib has none of this for
the Gaussian quantile. The full-support instances (MathlibUpstream.instIsOpenPosMeasureGaussianReal, 1-D, and
MathlibUpstream.instIsOpenPosMeasureStdGaussian, multivariate) come with the upstream drafts.
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
The interval split Φ b − Φ a = P(Ioc a b).
Φ is strictly monotone (MathlibUpstream.strictMono_cdf_gaussianReal).
Φ is continuous (MathlibUpstream.continuous_cdf_gaussianReal).
Gaussian symmetry Φ(−t) = 1 − Φ(t) (MathlibUpstream.cdf_gaussianReal_neg).
hmono discharged: the real quantile is monotone on (0,1) — larger p, larger
sub-level set, larger sSup.
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; smoothing_probit_lipschitz applies it to feed the Neyman–Pearson
bound its threshold.
hanti discharged: the real quantile is odd about ½, Φ⁻¹(1−q) = −Φ⁻¹(q) on
(0,1). Φ is injective, and symmetry plus stdNormalCDF_quantile send both sides to
1 − q.
Φ⁻¹(Φ s) = s — the quantile inverts the cdf everywhere (strict monotonicity makes
the strict sub-level set of Φ s exactly Iio s).
Φ 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).
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.