The standard normal distribution function and the probit

The standard normal distribution function Φ is the cdf of mathlib's gaussianReal 0 1, and everything about it here is an instance of a general fact about cdfs from Linglib/Core/Probability/CDF.lean. A nondegenerate Gaussian has no atoms, charges every nonempty open set, and is invariant under negation when centred, so Φ is continuous, strictly monotone and satisfies Φ (-x) = 1 - Φ x. It is therefore an order isomorphism from ℝ onto (0, 1), and the probit is its inverse, extended by 0 outside (0, 1) as Real.log is extended outside (0, ∞).

Main definitions

• ProbabilityTheory.normalCDF: the standard normal distribution function Φ.
• ProbabilityTheory.probit: the standard normal quantile function Φ⁻¹.

Main results

• ProbabilityTheory.cdf_gaussianReal_eq: standardization, cdf (gaussianReal μ v) x = Φ ((x - μ) / √v).
• ProbabilityTheory.gaussianReal_real_Ioi: the upper tail of a Gaussian is Φ ((μ - x) / √v).
• ProbabilityTheory.probit_one_sub: Φ⁻¹ (1 - p) = -Φ⁻¹ p, for every real p.
• ProbabilityTheory.gaussianPDFReal_div_gaussianPDFReal: the ratio of two Gaussian densities of a common variance is the exponential of an affine function.
• ProbabilityTheory.map_pi_gaussianReal_sum_mul, variance_pi_gaussianReal_sum_mul, covariance_pi_gaussianReal_sum_mul: a linear combination of independent Gaussians is Gaussian, with the variance and covariances read off the coefficients.

Implementation notes

Mathlib states the atomlessness of a Gaussian as a lemma with hypothesis v ≠ 0. The instances here take [NeZero v] instead, so that they fire for the standard normal gaussianReal 0 1. [UPSTREAM] candidates for Mathlib/Probability/Distributions/Gaussian/Real.lean, and the linear combination lemmas for Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean.

instance ProbabilityTheory.instNullSingletonClassRealGaussianRealOfNeZeroNNReal_linglib {μ : ℝ} {v : NNReal} [NeZero v] : MeasureTheory.NullSingletonClass (gaussianReal μ v)

theorem ProbabilityTheory.isOpenPosMeasure_gaussianReal {μ : ℝ} {v : NNReal} (hv : v ≠ 0) : (gaussianReal μ v).IsOpenPosMeasure

A nondegenerate Gaussian charges every nonempty open set.

instance ProbabilityTheory.instIsOpenPosMeasureRealGaussianRealOfNeZeroNNReal_linglib {μ : ℝ} {v : NNReal} [NeZero v] : (gaussianReal μ v).IsOpenPosMeasure

instance ProbabilityTheory.instIsNegInvariantRealGaussianRealOfNat_linglib {v : NNReal} : (gaussianReal 0 v).IsNegInvariant

The standard normal distribution function

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

The standard normal distribution function Φ, the cdf of gaussianReal 0 1.

Equations

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

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

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

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

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

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

theorem ProbabilityTheory.normalCDF_strictMono : StrictMono normalCDF

theorem ProbabilityTheory.normalCDF_monotone : Monotone normalCDF

theorem ProbabilityTheory.normalCDF_injective : Function.Injective normalCDF

theorem ProbabilityTheory.continuous_normalCDF : Continuous normalCDF

@[simp]

theorem ProbabilityTheory.range_normalCDF : Set.range normalCDF = Set.Ioo 0 1

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

The reflection formula Φ (-x) = 1 - Φ x.

@[simp]

theorem ProbabilityTheory.normalCDF_zero : normalCDF 0 = 2⁻¹

theorem ProbabilityTheory.inv_two_lt_normalCDF_iff {x : ℝ} : 2⁻¹ < normalCDF x ↔ 0 < x

theorem ProbabilityTheory.normalCDF_lt_inv_two_iff {x : ℝ} : normalCDF x < 2⁻¹ ↔ x < 0

Standardization

theorem ProbabilityTheory.cdf_gaussianReal_eq (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : ↑(cdf (gaussianReal μ v)) x = normalCDF ((x - μ) / √↑v)

The cdf of a nondegenerate Gaussian is Φ at the standard score.

theorem ProbabilityTheory.gaussianReal_real_Ioi (μ : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : (gaussianReal μ v).real (Set.Ioi x) = normalCDF ((μ - x) / √↑v)

The upper tail of a nondegenerate Gaussian X ~ N(μ, v) is P(X > x) = Φ ((μ - x) / √v).

The probit

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

The probit, the quantile function Φ⁻¹ of the standard normal, equal to the inverse of normalCDF on (0, 1) and to 0 elsewhere. The extension by 0 makes probit_one_sub hold for every real argument.

Equations

• ProbabilityTheory.probit p = if hp : p ∈ Set.Ioo 0 1 then (ProbabilityTheory.cdfOrderIso (ProbabilityTheory.gaussianReal 0 1)).symm ⟨p, hp⟩ else 0

theorem ProbabilityTheory.probit_of_mem {p : ℝ} (hp : p ∈ Set.Ioo 0 1) : probit p = (cdfOrderIso (gaussianReal 0 1)).symm ⟨p, hp⟩

theorem ProbabilityTheory.probit_of_notMem {p : ℝ} (hp : p ∉ Set.Ioo 0 1) : probit p = 0

theorem ProbabilityTheory.normalCDF_probit {p : ℝ} (hp : p ∈ Set.Ioo 0 1) : normalCDF (probit p) = p

@[simp]

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

theorem ProbabilityTheory.probit_lt_probit_iff {p q : ℝ} (hp : p ∈ Set.Ioo 0 1) (hq : q ∈ Set.Ioo 0 1) : probit p < probit q ↔ p < q

theorem ProbabilityTheory.probit_le_probit_iff {p q : ℝ} (hp : p ∈ Set.Ioo 0 1) (hq : q ∈ Set.Ioo 0 1) : probit p ≤ probit q ↔ p ≤ q

@[simp]

theorem ProbabilityTheory.probit_inv_two : probit 2⁻¹ = 0

theorem ProbabilityTheory.probit_one_sub (p : ℝ) : probit (1 - p) = -probit p

The probit is odd about 1 / 2. Outside (0, 1) both sides are the junk value 0.

Densities

theorem ProbabilityTheory.gaussianPDFReal_div_gaussianPDFReal (μ₁ μ₀ : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : gaussianPDFReal μ₁ v x / gaussianPDFReal μ₀ v x = Real.exp ((μ₁ - μ₀) * (x - (μ₀ + μ₁) / 2) / ↑v)

The ratio of two Gaussian densities of a common nonzero variance is the exponential of an affine function, zero midway between the means.

Linear combinations of independent Gaussians

theorem ProbabilityTheory.map_pi_gaussianReal_sum_mul {ι : Type u_1} [Fintype ι] (m : ι → ℝ) (v : ι → NNReal) (d : ι → ℝ) : MeasureTheory.Measure.map (fun (η : ι → ℝ) => ∑ i : ι, d i * η i) (MeasureTheory.Measure.pi fun (i : ι) => gaussianReal (m i) (v i)) = gaussianReal (∑ i : ι, d i * m i) (∑ i : ι, NNReal.mk (d i ^ 2) ⋯ * v i)

A linear combination of independent Gaussians is Gaussian.

theorem ProbabilityTheory.variance_pi_gaussianReal_sum_mul {ι : Type u_1} [Fintype ι] (m : ι → ℝ) (v : ι → NNReal) (d : ι → ℝ) : variance (fun (η : ι → ℝ) => ∑ i : ι, d i * η i) (MeasureTheory.Measure.pi fun (i : ι) => gaussianReal (m i) (v i)) = ∑ i : ι, d i ^ 2 * ↑(v i)

The variance of a linear combination of independent Gaussians.

theorem ProbabilityTheory.covariance_pi_gaussianReal_sum_mul {ι : Type u_1} [Fintype ι] (m : ι → ℝ) (v : ι → NNReal) (d e : ι → ℝ) : covariance (fun (η : ι → ℝ) => ∑ i : ι, d i * η i) (fun (η : ι → ℝ) => ∑ i : ι, e i * η i) (MeasureTheory.Measure.pi fun (i : ι) => gaussianReal (m i) (v i)) = ∑ i : ι, d i * e i * ↑(v i)

The covariance of two linear combinations of independent Gaussians.