Documentation

LeanMlir.Proofs.Certificates.GaussianQuantile

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 monotone, odd about ½, continuous and inverts Φ both ways; below 0 it takes the junk value 0. The IsOpenPosMeasure instances say the 1-D and the multivariate standard Gaussian charge every nonempty open set. Mathlib has none of this for the Gaussian quantile.

instance Proofs.instIsOpenPosMeasureRealGaussianRealOfNatNNReal_leanMlir :

(ProbabilityTheory.gaussianReal 0 1).IsOpenPosMeasure

N(0,1) charges every nonempty open set (the pdf is everywhere positive) — packaged as the Mathlib IsOpenPosMeasure class.

instance Proofs.stdGaussian.instIsOpenPosMeasure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] :

(ProbabilityTheory.stdGaussian E).IsOpenPosMeasure

The standard Gaussian on a finite-dimensional inner-product space charges every nonempty open set: it is the pushforward of the pi-Gaussian (open-pos by pi.isOpenPosMeasure) under the surjective continuous basis sum.

noncomputable def Proofs.stdNormalCDF :

The standard-normal CDF Φ — Mathlib's cdf of the genuine gaussianReal 0 1.

Equations

Proofs.stdNormalCDF t = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) t

Instances For

noncomputable def Proofs.stdNormalQuantile (p : ℝ) :

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

theorem Proofs.stdGaussian_Ioo_pos {s t : ℝ} (hst : s < t) :

0 < (ProbabilityTheory.gaussianReal 0 1) (Set.Ioo s t)

Every open interval carries positive standard-Gaussian mass (the pdf is everywhere positive). The engine of strict monotonicity.

theorem Proofs.stdNormalCDF_strictMono :

StrictMono stdNormalCDF

Φ is strictly monotone: Φ t − Φ s = P(Ioc s t) > 0 for s < t.

theorem Proofs.stdNormalCDF_neg (t : ℝ) :

stdNormalCDF (-t) = 1 - stdNormalCDF t

Gaussian symmetry Φ(−t) = 1 − Φ(t): the standard Gaussian is invariant under negation, so P(Iic (−t)) = P(Ici t), and (no atoms) the complement gives the rest.

theorem Proofs.stdNormalCDF_exists_lt {p : ℝ} (hp : 0 < p) :

∃ (t : ℝ), stdNormalCDF t < p

Φ → 0 at −∞, so for p > 0 some t has Φ t < p — the quantile's set is nonempty.

theorem Proofs.stdNormalCDF_exists_gt {p : ℝ} (hp : p < 1) :

∃ (t : ℝ), p < stdNormalCDF t

Φ → 1 at +∞, so for p < 1 some t has Φ t > p.

theorem Proofs.stdNormalCDF_sublevel_bddAbove {p : ℝ} (hp : p < 1) :

BddAbove {t : ℝ | stdNormalCDF t < p}

For p < 1 the sub-level set {Φ < p} is bounded above (anything past a point with Φ > p is excluded).

theorem Proofs.stdNormalQuantile_monotoneOn :

MonotoneOn stdNormalQuantile (Set.Ioo 0 1)

hmono discharged: the real quantile is monotone on (0,1) — larger p, larger sub-level set, larger sSup.

theorem Proofs.stdNormalCDF_sSup_lt_eq_sInf_gt {q : ℝ} (hq : q ∈ Set.Ioo 0 1) :

sSup {t : ℝ | stdNormalCDF t < q} = sInf {t : ℝ | q < stdNormalCDF t}

No flat step at level q: sSup {Φ < q} = sInf {Φ > q}. Any gap between them would contain two points where Φ = q exactly — impossible for a strictly monotone Φ. The bridge between the quantile's sSup form and its mirrored sInf form.

theorem Proofs.stdNormalQuantile_anti {q : ℝ} (hq : q ∈ Set.Ioo 0 1) :

stdNormalQuantile (1 - q) = -stdNormalQuantile q

hanti discharged: the real quantile is odd about ½, Φ⁻¹(1−q) = −Φ⁻¹(q) on (0,1). Symmetry turns {Φ < 1−q} into the negation of {Φ > q}, sSup ∘ neg into −sInf, and the no-flat-step lemma closes the sInf/sSup mismatch.

theorem Proofs.stdNormalCDF_quantile {p : ℝ} (hp : p ∈ Set.Ioo 0 1) :

stdNormalCDF (stdNormalQuantile p) = p

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 — G2's Neyman–Pearson bound enters through it.

theorem Proofs.stdNormalQuantile_cdf (s : ℝ) :

stdNormalQuantile (stdNormalCDF s) = s

Φ⁻¹(Φ s) = s — the quantile inverts the cdf everywhere (strict monotonicity makes the strict sub-level set of Φ s exactly Iio s).

theorem Proofs.stdNormalCDF_pos (s : ℝ) :

0 < stdNormalCDF s

Φ never reaches 0: there is Gaussian mass below every point.

theorem Proofs.stdNormalCDF_lt_one (s : ℝ) :

stdNormalCDF s < 1

Φ never reaches 1 (symmetry + stdNormalCDF_pos).

theorem Proofs.stdNormalCDF_mem_Ioo (s : ℝ) :

stdNormalCDF s ∈ Set.Ioo 0 1

Φ maps into the open unit interval.

theorem Proofs.stdNormalQuantile_strictMonoOn :

StrictMonoOn stdNormalQuantile (Set.Ioo 0 1)

Φ⁻¹ is STRICTLY monotone on (0,1) (upgrade of stdNormalQuantile_monotoneOn): reflect strictness through Φ via the two-sided inverse stdNormalCDF_quantile.

theorem Proofs.stdNormalQuantile_surjOn :

Set.SurjOn stdNormalQuantile (Set.Ioo 0 1) Set.univ

Φ⁻¹ maps (0,1) ONTO ℝ: every real s is Φ⁻¹(Φ s).

theorem Proofs.stdNormalQuantile_continuousAt {p : ℝ} (hp : p ∈ Set.Ioo 0 1) :

ContinuousAt stdNormalQuantile p

Φ⁻¹ is continuous at every p ∈ (0,1): strictly monotone on the open interval with image all of ℝ (a neighborhood of anything).

theorem Proofs.stdNormalQuantile_continuousOn :

ContinuousOn stdNormalQuantile (Set.Ioo 0 1)

Φ⁻¹ is continuous on (0,1).

theorem Proofs.stdNormalQuantile_of_nonpos {q : ℝ} (hq : q ≤ 0) :

stdNormalQuantile q = 0

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.