Standard Normal Distribution Infrastructure

Pure standard-normal infrastructure: density, CDF, monotonicity, symmetry, continuity, and the probit (inverse-CDF) function. Application-agnostic — used by Thurstone's discriminal-process theory, Signal Detection Theory, and any other consumer that needs Φ and Φ⁻¹ over the reals.

Definitions

• normalPDF: the standard normal density φ(t) = (1/√(2π)) exp(−t²/2)
• normalCDF: the standard normal CDF Φ(x) = ∫_{−∞}^{x} φ(t) dt
• probit: the standard-normal quantile function Φ⁻¹ (with junk value 0 outside (0, 1))

The CDF is defined via Mathlib's cdf (gaussianReal 0 1), grounding the properties in Mathlib's measure-theoretic Gaussian infrastructure.

Mathlib upstream candidates

None of normalCDF_neg, normalCDF_zero, normalCDF_strictMono, continuous_normalCDF, normalCDF_injective, normalCDF_surj_Ioo, or probit exist in mathlib (verified 2026-04-25 against Mathlib.Probability.CDF and Mathlib.Probability.Distributions.Gaussian.*). Mathlib provides only cdf_nonneg, cdf_le_one, monotone_cdf, and the tendsto_cdf_atBot/atTop limits at the level of generic probability measures. The continuous_cdf_of_noAtoms private lemma below is the strongest upstream candidate — it is generic for any atomless probability measure on ℝ.

Normal PDF

noncomputable def Core.normalPDF (t : ℝ) : ℝ

The standard normal probability density function: φ(t) = (1/√(2π)) · exp(-t²/2).

Equations

• Core.normalPDF t = 1 / √(2 * Real.pi) * Real.exp (-t ^ 2 / 2)

Normal CDF

noncomputable def Core.normalCDF (x : ℝ) : ℝ

The standard normal cumulative distribution function: Φ(x) = ∫_{-∞}^{x} (1/√(2π)) exp(-t²/2) dt.

Defined as cdf (gaussianReal 0 1) x, the CDF of the standard Gaussian measure evaluated at x.

Equations

• Core.normalCDF x = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x

Helper lemmas for the standard Gaussian

Properties

theorem Core.normalCDF_nonneg (x : ℝ) : 0 ≤ normalCDF x

The normal CDF is non-negative: Φ(x) ≥ 0 for all x.

theorem Core.normalCDF_le_one (x : ℝ) : normalCDF x ≤ 1

The normal CDF is at most 1: Φ(x) ≤ 1 for all x.

theorem Core.normalCDF_mono : Monotone normalCDF

The normal CDF is monotone increasing.

theorem Core.normalCDF_neg (x : ℝ) : normalCDF (-x) = 1 - normalCDF x

Symmetry: Φ(-x) = 1 - Φ(x).

theorem Core.normalCDF_zero : normalCDF 0 = 1 / 2

Φ(0) = 1/2 by symmetry of the standard normal distribution.

theorem Core.normalCDF_strictMono : StrictMono normalCDF

The normal CDF is strictly monotone increasing.

theorem Core.normalCDF_pos (x : ℝ) : 0 < normalCDF x

0 < Φ(x) for all x. The standard normal CDF takes values in the open interval (0, 1) everywhere on the reals.

Proof: pick the non-empty Ioc (x-1) x ⊆ Iic x and apply stdGaussian_real_Ioc_pos.

theorem Core.normalCDF_lt_one (x : ℝ) : normalCDF x < 1

Φ(x) < 1 for all x. Dual of normalCDF_pos via the symmetry Φ(-x) = 1 - Φ(x).

theorem Core.normalCDF_mem_Ioo (x : ℝ) : normalCDF x ∈ Set.Ioo 0 1

The standard normal CDF maps into Set.Ioo 0 1.

theorem Core.normalCDF_pos_gt_half {x : ℝ} (hx : 0 < x) : 1 / 2 < normalCDF x

For x > 0, Φ(x) > 1/2.

theorem Core.normalCDF_neg_lt_half {x : ℝ} (hx : x < 0) : normalCDF x < 1 / 2

For x < 0, Φ(x) < 1/2.

theorem Core.normalCDF_injective : Function.Injective normalCDF

The normal CDF is injective (from strict monotonicity).

Continuity and surjectivity

theorem Core.continuous_normalCDF : Continuous normalCDF

The standard normal CDF is continuous.

theorem Core.normalCDF_surj_Ioo (p : ℝ) (hp0 : 0 < p) (hp1 : p < 1) : ∃ (x : ℝ), normalCDF x = p

The standard normal CDF is surjective onto (0, 1): for any p ∈ (0, 1), there exists x with Φ(x) = p.

Probit (inverse normal CDF / quantile function)

noncomputable def Core.probit (p : ℝ) : ℝ

The probit function (inverse normal CDF / quantile of the standard normal): for p ∈ (0, 1), returns the unique x with Φ(x) = p. Returns the junk value 0 for inputs outside (0, 1).

Existence follows from the Intermediate Value Theorem applied to the continuous, strictly monotone normalCDF with limits 0 at -∞ and 1 at +∞.

Junk-value caveat: probit 0 = probit 1 = probit 2 = 0. Callers that might pass boundary or out-of-range values should guard with 0 < p < 1, or apply a continuity correction (e.g., the Hautus 1995 log-linear rule) before invoking.

Equations

• Core.probit p = if h : 0 < p ∧ p < 1 then Classical.choose ⋯ else 0

theorem Core.probit_spec {p : ℝ} (hp0 : 0 < p) (hp1 : p < 1) : normalCDF (probit p) = p

Specification: Φ(probit(p)) = p for p ∈ (0, 1).

theorem Core.probit_normalCDF (x : ℝ) : probit (normalCDF x) = x

Specification: probit(Φ(x)) = x for all x (left inverse).

theorem Core.probit_lt_iff {p₁ p₂ : ℝ} (hp₁_lo : 0 < p₁) (hp₁_hi : p₁ < 1) (hp₂_lo : 0 < p₂) (hp₂_hi : p₂ < 1) : probit p₁ < probit p₂ ↔ p₁ < p₂

On (0, 1), the probit ordering matches the input ordering exactly. Subsumes the strict-monotonicity direction (probit p₁ < probit p₂ when p₁ < p₂) as .mpr.

Order-iso packaging

The standard normal CDF is a strictly monotone bijection between ℝ and Set.Ioo (0 : ℝ) 1. Packaging this as an OrderIso gives downstream code access to OrderIso.lt_iff_lt, OrderIso.symm_apply_apply, etc. without the four 0 < pᵢ < 1 hypotheses that probit_lt_iff requires for the junk-value-tolerant API. Both APIs are kept: the bare probit_lt_iff is ergonomic for raw real inputs; the OrderIso is the structural form.

TODO: upstream as Real.normalCDFOrderIso : ℝ ≃o Set.Ioo (0:ℝ) 1 to Mathlib.Probability.Distributions.Gaussian.Real.

noncomputable def Core.normalCDFOrderIso : ℝ ≃o ↑(Set.Ioo 0 1)

The standard normal CDF as an order isomorphism ℝ ≃o Set.Ioo (0:ℝ) 1. Inverse is given by probit restricted to (0, 1).

Equations

• One or more equations did not get rendered due to their size.