Standard Normal CDF Infrastructure

@cite{luce-1959}

Shared Gaussian CDF definitions and properties used by both Thurstone's discriminal-process theory (§2.D) and Signal Detection Theory (§2.E) in @cite{luce-1959}.

Definitions

• normalPDF: the standard normal density φ(t) = (1/√(2π)) exp(−t²/2)
• normalCDF: the standard normal CDF Φ(x) = ∫_{−∞}^{x} φ(t) dt

Properties

Monotonicity, strict monotonicity, symmetry, boundary values, and bounds. The CDF is defined via Mathlib's cdf (gaussianReal 0 1), which gives normalCDF x = (gaussianReal 0 1).real (Iic x). This grounds the properties in Mathlib's measure-theoretic Gaussian infrastructure.

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)

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

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_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).

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.