The error function

This file defines the Gauss error function erf x = (2 / √π) * ∫ t in 0..x, exp (-t ^ 2) and its complement erfc x = 1 - erf x, and develops their elementary real-variable theory: oddness, strict monotonicity, the derivative, and the limits at both infinities.

These are the error-function targets of TauCetiRoadmap/StandardDistributions/README.md, Layer 2. The names and statement shapes follow those proposed for Mathlib in mathlib4#34053, so that the declarations here can be replaced by Mathlib's once it provides them. The identification erf x = regularizedGamma (1 / 2) (x ^ 2), which holds for 0 ≤ x — the right-hand side is even in x while erf is odd — needs the incomplete gamma function and is not proved here.

The limits at infinity come from Mathlib's Gaussian integral integral_gaussian_Ioi together with the improper-integral comparison MeasureTheory.intervalIntegral_tendsto_integral_Ioi; the derivative is the fundamental theorem of calculus for a continuous integrand.

Main declarations

• TauCeti.Real.erf and TauCeti.Real.erfc — the error function and its complement.
• TauCeti.Real.erf_neg — the error function is odd.
• TauCeti.Real.hasDerivAt_erf — its derivative is 2 / √π * exp (-x ^ 2).
• TauCeti.Real.strictMono_erf — it is strictly monotone.
• TauCeti.Real.tendsto_erf_atTop and TauCeti.Real.tendsto_erf_atBot — its limits are 1 and -1, whence TauCeti.Real.abs_erf_lt_one.

noncomputable def TauCeti.Real.erf (x : ℝ) : ℝ

The Gauss error function, erf x = (2 / √π) * ∫ t in 0..x, exp (-t ^ 2).

Equations

• TauCeti.Real.erf x = 2 / √Real.pi * ∫ (t : ℝ) in 0..x, Real.exp (-t ^ 2)

noncomputable def TauCeti.Real.erfc (x : ℝ) : ℝ

The complementary error function, erfc x = 1 - erf x.

Equations

• TauCeti.Real.erfc x = 1 - TauCeti.Real.erf x

theorem TauCeti.Real.erf_def (x : ℝ) : erf x = 2 / √Real.pi * ∫ (t : ℝ) in 0..x, Real.exp (-t ^ 2)

The defining integral formula for the error function.

theorem TauCeti.Real.erfc_def (x : ℝ) : erfc x = 1 - erf x

The defining formula for the complementary error function.

@[simp]

theorem TauCeti.Real.erf_zero : erf 0 = 0

The error function vanishes at the origin.

@[simp]

theorem TauCeti.Real.erfc_zero : erfc 0 = 1

The complementary error function is 1 at the origin.

@[simp]

theorem TauCeti.Real.erf_neg (x : ℝ) : erf (-x) = -erf x

The error function is odd.

@[simp]

theorem TauCeti.Real.erfc_neg (x : ℝ) : erfc (-x) = 2 - erfc x

The complementary error function reflects around the value 1.

theorem TauCeti.Real.hasStrictDerivAt_erf (x : ℝ) : HasStrictDerivAt erf (2 / √Real.pi * Real.exp (-x ^ 2)) x

The error function is strictly differentiable, with derivative 2 / √π * exp (-x ^ 2).

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

The derivative of the error function.

@[simp]

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

The derivative of the error function, in deriv form.

theorem TauCeti.Real.differentiable_erf : Differentiable ℝ erf

The error function is differentiable.

theorem TauCeti.Real.continuous_erf : Continuous erf

The error function is continuous.

theorem TauCeti.Real.hasStrictDerivAt_erfc (x : ℝ) : HasStrictDerivAt erfc (-(2 / √Real.pi * Real.exp (-x ^ 2))) x

The complementary error function is strictly differentiable, with derivative -(2 / √π * exp (-x ^ 2)).

theorem TauCeti.Real.hasDerivAt_erfc (x : ℝ) : HasDerivAt erfc (-(2 / √Real.pi * Real.exp (-x ^ 2))) x

The derivative of the complementary error function.

@[simp]

theorem TauCeti.Real.deriv_erfc : deriv erfc = fun (x : ℝ) => -(2 / √Real.pi * Real.exp (-x ^ 2))

The derivative of the complementary error function, in deriv form.

theorem TauCeti.Real.differentiable_erfc : Differentiable ℝ erfc

The complementary error function is differentiable.

theorem TauCeti.Real.continuous_erfc : Continuous erfc

The complementary error function is continuous.

theorem TauCeti.Real.strictMono_erf : StrictMono erf

The error function is strictly increasing.

theorem TauCeti.Real.strictAnti_erfc : StrictAnti erfc

The complementary error function is strictly decreasing.

theorem TauCeti.Real.erf_pos {x : ℝ} (hx : 0 < x) : 0 < erf x

The error function is positive on the positive half-line.

theorem TauCeti.Real.erf_nonneg {x : ℝ} (hx : 0 ≤ x) : 0 ≤ erf x

The error function is nonnegative on the nonnegative half-line.

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

The error function tends to 1 at +∞.

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

The error function tends to -1 at -∞.

theorem TauCeti.Real.tendsto_erfc_atTop : Filter.Tendsto erfc Filter.atTop (nhds 0)

The complementary error function tends to 0 at +∞.

theorem TauCeti.Real.tendsto_erfc_atBot : Filter.Tendsto erfc Filter.atBot (nhds 2)

The complementary error function tends to 2 at -∞.

theorem TauCeti.Real.erf_le_one (x : ℝ) : erf x ≤ 1

The error function is bounded above by 1.

theorem TauCeti.Real.erf_lt_one (x : ℝ) : erf x < 1

The error function never attains the value 1.

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

The error function never attains the value -1.

theorem TauCeti.Real.abs_erf_lt_one (x : ℝ) : |erf x| < 1

The error function takes values in the open interval (-1, 1).

theorem TauCeti.Real.erfc_pos (x : ℝ) : 0 < erfc x

The complementary error function is positive.

theorem TauCeti.Real.erfc_lt_two (x : ℝ) : erfc x < 2

The complementary error function is bounded above by 2, strictly.