gaussian_tail

A3 — the Gaussian tail-integral lemma (reachable half of the CVaR obligation)

Seal

Obligation A3 (reachable half) · Status sealed — all five public declarations are axiom-clean (#print axioms verbatim in The machine seal), no sorryAx, no interface hypothesis anywhere in the module. Elaborated via lake env lean on the build copy; no lake build, no shared-file edits (orchestrator integrates into Ctrllib.lean).
Links: module index · risk map [(/Code/tasks/streams/risk_aware_planning/proof_obligations_risk_phases.md)] rows A3 · §7 item 4 · §8 walls · SymPy pin [(/Code/tasks/streams/ctrllib/scratch/pin_gaussian_tail.py)] · source rockafellar2000optimization

What this seals, in one paragraph

For the standard normal density $\phi (w)=e^{-w^2/2}/\sqrt{2\pi }$, this module proves the improper tail integral

${\int }_q^{\infty }w\phi (w)dw=\phi (q).$

This is the one closed-form fact the Gaussian CVaR expression rests on that is reachable in Mathlib. The full closed form additionally needs ${\Phi }^{-1}$ (the inverse Gaussian CDF / probit), which is absent from Mathlib — a documented wall, stated below and never attempted. The density is stated on Mathlib’s own ProbabilityTheory.gaussianPDFReal 0 1 (mean $0$, variance $1$); the derivative algebra runs on the explicit form stdNormalPdf and is joined by the proved bridge lemma stdNormalPdf_eq (no bridge is assumed).

The statement and its objects

The public API of GaussianTail.lean:

• stdNormalPdf (w) := Real.exp (-(w ^ 2) / 2) / Real.sqrt (2 * π) — the explicit standard-normal density $\phi$. The exponent is written fully parenthesized, -(w ^ 2) / 2, so it matches the derivative chain term-for-term.
• stdNormalPdf_eq : stdNormalPdf w = gaussianPDFReal 0 1 w — the proved bridge. gaussianPDFReal 0 1 w unfolds to $(\sqrt{2\pi \cdot 1}{)}^{-1}{e}^{-(w-0{)}^2/(2\cdot 1)}$; after NNReal.coe_one, mul_one, sub_zero this is exactly $\phi (w)$, closed by ring.
• integral_Ioi_mul_gaussianPDFReal (q) : ∫ w in Ioi q, w * gaussianPDFReal 0 1 w = gaussianPDFReal 0 1 q — the tail-integral lemma, stated on Mathlib’s density.

Three sealed helpers carry the FTC-2 hypotheses: hasDerivAt_neg_stdNormalPdf (the antiderivative), integrable_mul_stdNormalPdf_Ioi (integrability on the tail), tendsto_neg_stdNormalPdf (vanishing at $+\infty$).

Role in the Gaussian closed-form CVaR

The Gaussian conditional value-at-risk has the closed form

${\mathrm{CVaR}}_{\alpha }=\mu +\sigma \frac{\phi ({\Phi }^{-1}(\alpha ))}{1-\alpha }.$

Its derivation reduces, after the standardization $Z=(X-\mu )/\sigma$, to the conditional tail mean $\mathbb{E}[Z\mid Z>q]=\frac{1}{1-\Phi (q)}{\int }_q^{\infty }w\phi (w)dw$, and the numerator is exactly the integral sealed here — it collapses to $\phi (q)$ because $-\phi$ is an antiderivative of $w\phi (w)$. Setting the tail level $q={\Phi }^{-1}(\alpha )$ and $1-\Phi (q)=1-\alpha$ yields the closed form. The tail integral is the analytic core; the $\alpha$-parametrization is the wall.

The Φ⁻¹ wall (honest boundary)

The closed form as written cannot be stated in Lean without first building the Gaussian quantile. Per the risk map’s Mathlib ledger [(~/Code/tasks/streams/risk_aware_planning/proof_obligations_risk_phases.md)] (§0 and §8):

• Φ⁻¹ / probit / quantile: ABSENT (rg -i "quantile", "\berf\b" → 0 hits repo-wide).
• The Gaussian CDF itself is statable — the generic cdf (μ : Measure ℝ) applies to gaussianReal — but it has no inverse.

So A3 splits, honestly: the tail integral is this sealed [NEW] stone; the ${\Phi }^{-1}$ parametrization stays a [WALL], settled in the pipeline (the constant $k_{\alpha }=\phi ({\Phi }^{-1}(\alpha ))/(1-\alpha )$ comes from scipy.stats.norm, desk-checked against the empirical tail mean). This module does not attempt the wall.

Proof route — antiderivative + FTC-2 on a half-line

The mechanism is the fundamental theorem of calculus on $(q,\infty )$. Since

$\frac{d}{dw}[-\phi (w)]=w\phi (w)\text{and}\phi (w)\to 0\text{ as }w\to +\infty ,$

the improper integral telescopes: ${\int }_q^{\infty }w\phi (w)dw=[-\phi (w){]}_q^{\infty }=-\phi (\infty )+\phi (q)=\phi (q)$.

Mathlib lemmas load-bearing in the proof:

Step	Mathlib lemma
FTC-2 engine on $(a,\infty )$: ${\int }_a^{\infty }{f}^{\prime }=m-f(a)$	MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto'
Antiderivative $\frac{d}{dw}{e}^{-w^2/2}=e^{-w^2/2}(-w)$	HasDerivAt.exp, hasDerivAt_pow, HasDerivAt.div_const, HasDerivAt.neg
Tail integrability of $w{e}^{-w^2/2}$	integrable_mul_exp_neg_mul_sq (with $b=1/2$), Integrable.const_mul
Vanishing at $+\infty$: $e^{-w^2/2}\to 0$	Real.tendsto_exp_atBot, tendsto_pow_atTop, Tendsto.atTop_div_const_of_neg, Tendsto.div_const
Density bridge to gaussianPDFReal	NNReal.coe_one, plus ring

The FTC-2 engine is applied with $f=-\phi$, $f^{\prime }=w\mapsto w\phi (w)$, $a=q$, $m=0$; it returns $0-(-\phi (q))=\phi (q)$.

SymPy pin

Pin [(~/Code/tasks/streams/ctrllib/scratch/pin_gaussian_tail.py)] (run under new-pin-env) confirms, before any Lean:

• symbolic integrate(w*phi, (w, q, oo)) - phi(q) == 0 (exact);
• antiderivative identity d/dw[-phi] - w*phi == 0 (exact);
• ${\lim }_{w\to \infty }\phi (w)=0$;
• three numeric spot values ($q=-1,0,1.5$) matching $\phi (q)$ to $<10^{-12}$.

The machine seal

GaussianTail.lean holds stdNormalPdf and the five public results above. Elaboration is clean under ~/.elan/bin/lake --dir=~/lean/ctrllib env lean on the build copy ~/lean/ctrllib/Ctrllib/GaussianTail.lean; this directory’s GaussianTail.lean is the tracked source of truth. #print axioms for every public declaration, verbatim:

'Ctrllib.integral_Ioi_mul_gaussianPDFReal' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.stdNormalPdf_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.hasDerivAt_neg_stdNormalPdf' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.integrable_mul_stdNormalPdf_Ioi' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.tendsto_neg_stdNormalPdf' depends on axioms: [propext, Classical.choice, Quot.sound]

No sorryAx; the set is $\subseteq \{$propext, Classical.choice, Quot.sound$\}$ — the Mathlib-standard base.

Note on tags

No tag is set. The closed lean-wiki vocabulary is entirely control-theory categories (lyapunov, lasalle, passivity, comparison, matrix, cascade, dynamics); none names a probability tail integral, so per the tagging fallback the field is omitted rather than mislabel the page.