The Gauss error function

Mathlib has no error function, so this module defines erf x = 2 / √π ∫₀ˣ exp (-t²) dt on the reals. It proves the facts that torch.erf and the exact GELU rely on: erf 0 = 0, oddness, the derivative 2 / √π exp (-x²), strict monotonicity, and the limits 1 at +∞ and -1 at -∞, hence -1 < erf x < 1.

References

• NIST Digital Library of Mathematical Functions, section 7.2, error functions: https://dlmf.nist.gov/7.2

noncomputable def Spec.erf (x : ℝ) : ℝ

The Gauss error function, 2 / √π ∫₀ˣ exp (-t²) dt.

theorem Spec.continuous_exp_neg_sq : Continuous fun (t : ℝ) => Real.exp (-t ^ 2)

The Gaussian integrand is continuous.

@[simp]

theorem Spec.erf_zero : erf 0 = 0

The error function vanishes at zero.

theorem Spec.erf_neg (x : ℝ) : erf (-x) = -erf x

The error function is odd.

theorem Spec.hasDerivAt_erf (x : ℝ) : HasDerivAt erf (2 / √Real.pi * Real.exp (-x ^ 2)) x

The derivative of the error function is 2 / √π exp (-x²).

theorem Spec.deriv_erf (x : ℝ) : deriv erf x = 2 / √Real.pi * Real.exp (-x ^ 2)

deriv erf is the scaled Gaussian.

theorem Spec.differentiable_erf : Differentiable ℝ erf

The error function is differentiable everywhere.

theorem Spec.continuous_erf : Continuous erf

The error function is continuous.

theorem Spec.strictMono_erf : StrictMono erf

The error function is strictly increasing.

theorem Spec.tendsto_erf_atTop : Filter.Tendsto erf Filter.atTop (nhds 1)

The error function tends to 1 at +∞.

theorem Spec.tendsto_erf_atBot : Filter.Tendsto erf Filter.atBot (nhds (-1))

The error function tends to -1 at -∞.

theorem Spec.erf_lt_one (x : ℝ) : erf x < 1

The error function stays below 1.

theorem Spec.neg_one_lt_erf (x : ℝ) : -1 < erf x

The error function stays above -1.