feat: Add error function (erf) and complementary error function (erfc)

[christian-oudard]

Summary

I was doing some finance math and needed the Error Function, so I thought I'd contribute it.

Main definitions

• Real.erf: The error function, defined as (2/√π) ∫₀ˣ e^(-t²) dt
• Real.erfc: The complementary error function, defined as 1 - erf x

Main results

• Real.erf_zero: erf 0 = 0
• Real.erf_neg: erf is an odd function: erf (-x) = -erf x
• Real.erf_tendsto_one: erf x → 1 as x → ∞
• Real.erf_tendsto_neg_one: erf x → -1 as x → -∞
• Real.erf_le_one: erf x ≤ 1 for all x
• Real.neg_one_le_erf: -1 ≤ erf x for all x
• Real.deriv_erf: deriv erf x = (2/√π) * exp(-x²)
• Real.differentiable_erf: erf is differentiable
• Real.continuous_erf: erf is continuous
• Real.strictMono_erf: erf is strictly monotone

Also adds erf to docs/overview.yaml under Special Functions.

---

• Builds successfully
• lake exe runLinter passes
• lake exe mk_all --check passes

[github-actions]

PR summary 95093e961c

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Analysis.SpecialFunctions.Erf (new file)	2503

---

Declarations diff

+ antitone_erfc
+ continuous_erf
+ continuous_erfc
+ deriv_erf
+ deriv_erfc
+ differentiable_erf
+ differentiable_erfc
+ erf
+ erf_le_one
+ erf_neg
+ erf_nonneg_of_nonneg
+ erf_tendsto_neg_one
+ erf_tendsto_one
+ erf_zero
+ erfc
+ erfc_le_one_of_nonneg
+ erfc_le_two
+ erfc_neg
+ erfc_nonneg
+ erfc_tendsto_two
+ erfc_tendsto_zero
+ erfc_zero
+ exp_neg_sq_even
+ hasDerivAt_erf
+ hasDerivAt_erfc
+ integral_exp_neg_sq_Ioi
+ monotone_erf
+ neg_one_le_erf
+ strictAnti_erfc
+ strictMono_erf

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[christian-oudard]

I'm a bit new to Lean and I was relying on LLMs for the details of this, so please review with that in mind.

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[plp127]

I wonder if we can get a complex error function somehow? It would be an antiderivative of (2/√π) e^(-z²) taking the value 0 for z = 0.

[plp127]

Suggested change

	noncomputable section
	public noncomputable section

so the results can be used in other files