The cumulative distribution function of a real Gaussian law

This file computes ProbabilityTheory.cdf (gaussianReal m v) in closed form. For a nonzero variance the answer is (1 + erf ((x - m) / √(2 * v))) / 2, and at the singular boundary v = 0 the law is a Dirac mass, with the step-function cdf.

These are the Gaussian entries of the closed-form cdf target of TauCetiRoadmap/StandardDistributions/README.md, Layer 2.

The computation goes through the interval integral of gaussianPDFReal, which is an affine change of variables away from the integral defining TauCeti.Real.erf; the improper integral over Set.Iic x is then the limit of those interval integrals, using TauCeti.Real.tendsto_erf_atBot for the contribution at -∞.

Main declarations

• TauCeti.Probability.intervalIntegral_gaussianPDFReal — the Gaussian density integrates to a difference of error-function values.
• TauCeti.Probability.integral_Iic_gaussianPDFReal — the same over a left half-line.
• TauCeti.Probability.cdf_gaussianReal_eq — the closed-form cdf for a nonzero variance.
• TauCeti.Probability.cdf_gaussianReal_zero_one — the standard Gaussian cdf.
• TauCeti.Probability.cdf_gaussianReal_eq_cdf_zero_one — standardization Φ ((x - m) / √v).
• TauCeti.Probability.cdf_gaussianReal_zero — the cdf at the singular boundary v = 0.
• TauCeti.Probability.cdf_gaussianReal_zero_one_neg — the symmetry Φ (-x) = 1 - Φ x of the standard Gaussian cdf.
• TauCeti.Probability.gaussianReal_preimage_Ioo_pos, TauCeti.Probability.measureReal_gaussianReal_preimage_Iic_lt, TauCeti.Probability.measureReal_gaussianReal_pos — for a nonzero variance every nondegenerate interval with extended bounds has positive mass.
• TauCeti.Probability.measureReal_gaussianReal_eq_cdf_zero_one — the mass of an interval with finite bounds as a difference of standard Gaussian cdf values.
• TauCeti.Probability.cdf_gaussianReal_self — for a nonzero variance the cdf equals 1 / 2 at the mean.
• TauCeti.Probability.cdf_gaussianReal_pos, TauCeti.Probability.cdf_gaussianReal_lt_one — for a nonzero variance the cdf takes values strictly between 0 and 1.
• TauCeti.Probability.strictMono_cdf_gaussianReal — for a nonzero variance the cdf is strictly increasing.
• TauCeti.Probability.hasDerivAt_cdf_gaussianReal — the cdf has the Gaussian density as its derivative.
• TauCeti.Probability.hasDerivAt_measureReal_gaussianReal_preimage_Iic, TauCeti.Probability.hasDerivAt_measureReal_gaussianReal — as a function of the mean, the mass up to an extended bound, and the mass of an interval with extended bounds, have the Gaussian densities at the bounds (TauCeti.Probability.gaussianPDFRealEReal) as derivative.
• TauCeti.Probability.measureReal_Ioi_gaussianReal — the upper tail, in terms of TauCeti.Real.erfc.
• TauCeti.Probability.measureReal_Ioi_gaussianReal_eq_cdf — the upper tail, in terms of the standard Gaussian cdf.
• TauCeti.Probability.mul_gaussianPDFReal_add_le_measureReal_Ioi_gaussianReal — a lower bound for the upper tail to the right of the mean, by the density at a later point.
• TauCeti.Probability.gaussianPDFReal_add_one_le_measureReal_map_abs_Ioi — the corresponding lower bound for the upper tail of the absolute value of a standard Gaussian.
• TauCeti.Probability.measureReal_le_of_hasLaw_gaussianReal — the random-variable corollary.

theorem TauCeti.Probability.intervalIntegral_gaussianPDFReal (m : ℝ) {v : NNReal} (a b : ℝ) : ∫ (t : ℝ) in a..b, ProbabilityTheory.gaussianPDFReal m v t = (Real.erf ((b - m) / √(2 * ↑v)) - Real.erf ((a - m) / √(2 * ↑v))) / 2

On an interval, the Gaussian density integrates to the difference of two error-function values. Both sides vanish at zero variance; otherwise the affine change of variables t ↦ (t - m) / √(2 * v) turns the integral into the one defining TauCeti.Real.erf.

theorem TauCeti.Probability.integral_Iic_gaussianPDFReal (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : ∫ (t : ℝ) in Set.Iic x, ProbabilityTheory.gaussianPDFReal m v t = (1 + Real.erf ((x - m) / √(2 * ↑v))) / 2

Over a left half-line, the Gaussian density integrates to (1 + erf ((x - m) / √(2 * v))) / 2.

theorem TauCeti.Probability.cdf_gaussianReal_eq (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v)) x = (1 + Real.erf ((x - m) / √(2 * ↑v))) / 2

The cumulative distribution function of a Gaussian law with nonzero variance.

theorem TauCeti.Probability.cdf_gaussianReal_zero_one (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x = (1 + Real.erf (x / √2)) / 2

The cumulative distribution function of the standard Gaussian law.

theorem TauCeti.Probability.cdf_gaussianReal_eq_cdf_zero_one (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v)) x = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((x - m) / √↑v)

A Gaussian cumulative distribution function of nonzero variance is the standard one at the standardized argument: P(X ≤ x) = Φ ((x - m) / √v) for X ∼ N(m, v).

theorem TauCeti.Probability.gaussianReal_preimage_Ioo_pos (m : ℝ) {v : NNReal} (hv : v ≠ 0) {l r : EReal} (hlr : l < r) : 0 < (ProbabilityTheory.gaussianReal m v) (Real.toEReal ⁻¹' Set.Ioo l r)

At positive variance, the open interval with extended bounds l < r has positive Gaussian mass.

theorem TauCeti.Probability.measureReal_gaussianReal_preimage_Iic_lt {m : ℝ} {v : NNReal} (hv : v ≠ 0) {l r : EReal} (hlr : l < r) : (ProbabilityTheory.gaussianReal m v).real (Real.toEReal ⁻¹' Set.Iic l) < (ProbabilityTheory.gaussianReal m v).real (Real.toEReal ⁻¹' Set.Iic r)

At positive variance, the Gaussian mass up to an extended bound is strictly increasing in the bound.

theorem TauCeti.Probability.cdf_gaussianReal_zero (m x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m 0)) x = if m ≤ x then 1 else 0

At the singular boundary v = 0 the Gaussian law is a Dirac mass, and its cumulative distribution function is the corresponding step function.

theorem TauCeti.Probability.cdf_gaussianReal_zero_one_neg (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) (-x) = 1 - ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x

The standard Gaussian cumulative distribution function is symmetric about zero: Φ (-x) = 1 - Φ x.

@[simp]

theorem TauCeti.Probability.cdf_gaussianReal_self (m : ℝ) {v : NNReal} (hv : v ≠ 0) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v)) m = 1 / 2

A Gaussian law with nonzero variance has its mean as median: its cumulative distribution function takes the value 1 / 2 at the mean.

theorem TauCeti.Probability.cdf_gaussianReal_pos (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : 0 < ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v)) x

The cumulative distribution function of a Gaussian law with nonzero variance is positive.

theorem TauCeti.Probability.cdf_gaussianReal_lt_one (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v)) x < 1

The cumulative distribution function of a Gaussian law with nonzero variance is less than one.

theorem TauCeti.Probability.strictMono_cdf_gaussianReal (m : ℝ) {v : NNReal} (hv : v ≠ 0) : StrictMono ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v))

The cumulative distribution function of a Gaussian law with nonzero variance is strictly increasing.

theorem TauCeti.Probability.hasDerivAt_cdf_gaussianReal (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : HasDerivAt (↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal m v))) (ProbabilityTheory.gaussianPDFReal m v x) x

The cumulative distribution function of a Gaussian law with nonzero variance has the Gaussian density as its derivative.

theorem TauCeti.Probability.measureReal_gaussianReal_pos (m : ℝ) {v : NNReal} (hv : v ≠ 0) {l r : EReal} {s : Set ℝ} (hlr : l < r) (hs₁ : Real.toEReal ⁻¹' Set.Ioo l r ⊆ s) : 0 < (ProbabilityTheory.gaussianReal m v).real s

At positive variance, every set containing the open interval with extended bounds l < r has positive Gaussian mass.

theorem TauCeti.Probability.measureReal_gaussianReal_eq_cdf_zero_one (m : ℝ) {v : NNReal} (hv : v ≠ 0) {l r : ℝ} {s : Set ℝ} (hlr : l ≤ r) (hs₁ : Set.Ioo l r ⊆ s) (hs₂ : s ⊆ Set.Icc l r) : (ProbabilityTheory.gaussianReal m v).real s = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((r - m) / √↑v) - ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((l - m) / √↑v)

At positive variance, the Gaussian mass of a set between the open and the closed interval with finite bounds l ≤ r is a difference of standard Gaussian cdf values.

theorem TauCeti.Probability.hasDerivAt_measureReal_gaussianReal_preimage_Iic {v : NNReal} (hv : v ≠ 0) (e : EReal) (μ : ℝ) : HasDerivAt (fun (μ : ℝ) => (ProbabilityTheory.gaussianReal μ v).real (Real.toEReal ⁻¹' Set.Iic e)) (-gaussianPDFRealEReal μ v e) μ

At positive variance, the Gaussian mass up to an extended bound e, as a function of the mean, has derivative minus the Gaussian density at e.

theorem TauCeti.Probability.hasDerivAt_measureReal_gaussianReal {v : NNReal} (hv : v ≠ 0) {l r : EReal} {s : Set ℝ} (hlr : l ≤ r) (hs₁ : Real.toEReal ⁻¹' Set.Ioo l r ⊆ s) (hs₂ : s ⊆ Real.toEReal ⁻¹' Set.Icc l r) (μ : ℝ) : HasDerivAt (fun (μ : ℝ) => (ProbabilityTheory.gaussianReal μ v).real s) (gaussianPDFRealEReal μ v l - gaussianPDFRealEReal μ v r) μ

At positive variance, the Gaussian mass of a set between the open and the closed interval with extended bounds l ≤ r, as a function of the mean, has derivative the difference of the Gaussian densities at the two bounds.

theorem TauCeti.Probability.measureReal_Ioi_gaussianReal (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : (ProbabilityTheory.gaussianReal m v).real (Set.Ioi x) = Real.erfc ((x - m) / √(2 * ↑v)) / 2

The upper tail of a Gaussian law with nonzero variance is half the complementary error function.

theorem TauCeti.Probability.measureReal_Ioi_gaussianReal_eq_cdf (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : (ProbabilityTheory.gaussianReal m v).real (Set.Ioi x) = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((m - x) / √↑v)

The upper tail of a Gaussian law with nonzero variance is a value of the standard Gaussian cumulative distribution function: P(X > x) = Φ ((m - x) / √v) for X ∼ N(m, v).

theorem TauCeti.Probability.integral_Ioi_gaussianPDFReal_eq_cdf (m : ℝ) {v : NNReal} (hv : v ≠ 0) (x : ℝ) : ∫ (t : ℝ) in Set.Ioi x, ProbabilityTheory.gaussianPDFReal m v t = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) ((m - x) / √↑v)

Over a right half-line, a Gaussian density of nonzero variance integrates to a value of the standard Gaussian cumulative distribution function: ∫ t in Ioi x, N(m, v)(t) = Φ ((m - x) / √v).

theorem TauCeti.Probability.mul_gaussianPDFReal_add_le_measureReal_Ioi_gaussianReal {m s t : ℝ} (v : NNReal) (hs : m ≤ s) : t * ProbabilityTheory.gaussianPDFReal m v (s + t) ≤ (ProbabilityTheory.gaussianReal m v).real (Set.Ioi s)

A lower bound for the upper tail of a Gaussian law: beyond a point s to the right of the mean, the interval (s, s + t] alone carries mass at least its length t times the density at its right end (for t < 0 the left side is nonpositive and the bound is trivial).

theorem TauCeti.Probability.gaussianPDFReal_add_one_le_measureReal_map_abs_Ioi {s : ℝ} (hs : 0 ≤ s) : ProbabilityTheory.gaussianPDFReal 0 1 (s + 1) ≤ (MeasureTheory.Measure.map (fun (x : ℝ) => |x|) (ProbabilityTheory.gaussianReal 0 1)).real (Set.Ioi s)

The absolute value of a standard Gaussian exceeds s ≥ 0 with probability at least the standard Gaussian density at s + 1.

theorem TauCeti.Probability.measureReal_le_of_hasLaw_gaussianReal {Ω : Type u_1} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω} {X : Ω → ℝ} (m : ℝ) {v : NNReal} (hv : v ≠ 0) (hX : ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal m v) P) (x : ℝ) : P.real {ω : Ω | X ω ≤ x} = (1 + Real.erf ((x - m) / √(2 * ↑v))) / 2

A random variable with a Gaussian law of nonzero variance has the error-function cumulative distribution function.