Documentation

LeanMlir.Proofs.Architectures.GeluErfGaussian

gaussPhi is the standard normal CDF #

GeluErf writes the density and the CDF in closed form over the interval integral, so the modules that import the exact GELU do not carry the probability library. This file ties both to Mathlib's Gaussian:

The ½ in gaussPhi's definition is integral_Iic_zero_gaussPdf: the density is even and integrates to one.

source
theorem Proofs.gaussPdf_eq_gaussianPDFReal (x : ℝ) :
gaussPdf x = ProbabilityTheory.gaussianPDFReal 0 1 x

gaussPdf is Mathlib's Gaussian density at mean 0, variance 1.

source
theorem Proofs.gaussPdf_integrable :
MeasureTheory.Integrable gaussPdf MeasureTheory.volume

gaussPdf is integrable over the line.

source
theorem Proofs.integral_Iic_zero_gaussPdf :
∫ (t : ℝ) in Set.Iic 0, gaussPdf t = 1 / 2

Half the mass lies below zero — the density is even and integrates to one.

source
theorem Proofs.gaussPhi_eq_measureReal_Iic (x : ℝ) :
gaussPhi x = (ProbabilityTheory.gaussianReal 0 1).real (Set.Iic x)

gaussPhi is the standard normal's mass on (−∞, x].

source
theorem Proofs.gaussPhi_eq_cdf (x : ℝ) :
gaussPhi x = ↑(ProbabilityTheory.cdf (ProbabilityTheory.gaussianReal 0 1)) x

gaussPhi is the CDF of the standard normal, as Mathlib defines both.