Affine Arithmetic: Transcendental Functions

This file implements transcendental functions for Affine Arithmetic using Chebyshev linearization combined with Taylor bounds.

Key Functions

• AffineForm.exp - Exponential function
• AffineForm.tanh - Hyperbolic tangent (crucial for GELU)
• AffineForm.log - Natural logarithm (for LogSumExp)

Linearization Strategy

For exp(x) on [a, b]:

1. The secant line through (a, e^a) and (b, e^b) gives an upper bound
2. The tangent at the midpoint gives a lower bound
3. We use the midpoint tangent as the linear approximation with error bounds

For tanh(x):

1. tanh is bounded in [-1, 1]
2. For small x, tanh(x) ≈ x is a good approximation
3. For larger x, we use the secant/tangent approach

Exponential Function

def LeanCert.Engine.Affine.AffineForm.exp (a : AffineForm) (taylorDepth : ℕ := 8) : AffineForm

Exponential using interval evaluation (loses correlation).

For tighter bounds, use expChebyshev which preserves linear terms.

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.expChebyshev (a : AffineForm) (taylorDepth : ℕ := 8) : AffineForm

Chebyshev linearization for exp(x) on [lo, hi].

Key insight: exp is convex, so the tangent line at any point is a lower bound. We use the tangent at the midpoint m: L(x) = e^m + e^m·(x - m) = e^m·(1 + x - m)

The error is bounded by the difference between the secant and tangent.

Equations

• One or more equations did not get rendered due to their size.

Hyperbolic Tangent

def LeanCert.Engine.Affine.AffineForm.tanh (a : AffineForm) : AffineForm

tanh using interval evaluation.

tanh(x) = (e^x - e^{-x}) / (e^x + e^{-x}) Always bounded in (-1, 1).

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.tanhChebyshev (a : AffineForm) : AffineForm

Chebyshev linearization for tanh(x).

tanh'(x) = 1 - tanh²(x) = sech²(x)

For small x: tanh(x) ≈ x with error O(x³) For large |x|: tanh(x) ≈ ±1

We use the tangent at midpoint as approximation.

Equations

• One or more equations did not get rendered due to their size.

Natural Logarithm

noncomputable def LeanCert.Engine.Affine.AffineForm.log (a : AffineForm) (_taylorDepth : ℕ := 8) : AffineForm

Logarithm using interval evaluation (requires positive input).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanCert.Engine.Affine.AffineForm.logChebyshev (a : AffineForm) (hpos : 0 < a.toInterval.lo) : AffineForm

Chebyshev linearization for log(x) on [lo, hi] with lo > 0.

log'(x) = 1/x, so tangent at m is: L(x) = log(m) + (x - m)/m

Equations

• One or more equations did not get rendered due to their size.

Hyperbolic Functions

def LeanCert.Engine.Affine.AffineForm.sinh (a : AffineForm) (taylorDepth : ℕ := 8) : AffineForm

Hyperbolic sine: sinh(x) = (e^x - e^{-x})/2

Computed via interval sinh bounds (no correlation).

Equations

• One or more equations did not get rendered due to their size.

def LeanCert.Engine.Affine.AffineForm.cosh (a : AffineForm) (taylorDepth : ℕ := 8) : AffineForm

Hyperbolic cosine: cosh(x) = (e^x + e^{-x})/2

Computed via interval cosh bounds. Always ≥ 1.

Equations

• One or more equations did not get rendered due to their size.

Soundness Theorems

theorem LeanCert.Engine.Affine.AffineForm.mem_exp {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : a.mem_affine eps v) (taylorDepth : ℕ) : (a.exp taylorDepth).mem_affine eps (Real.exp v)

exp is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_tanh {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : a.mem_affine eps v) : a.tanh.mem_affine eps (Real.tanh v)

tanh is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_sinh {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : a.mem_affine eps v) (taylorDepth : ℕ) : (a.sinh taylorDepth).mem_affine eps (Real.sinh v)

sinh is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_cosh {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : a.mem_affine eps v) (taylorDepth : ℕ) : (a.cosh taylorDepth).mem_affine eps (Real.cosh v)

cosh is sound

theorem LeanCert.Engine.Affine.AffineForm.mem_log {taylorDepth : ℕ} {a : AffineForm} {eps : NoiseAssignment} {v : ℝ} (hvalid : validNoise eps) (hmem : a.mem_affine eps v) (_hv_pos : 0 < v) (hI_pos : 0 < a.toInterval.lo) (_taylorDepth : ℕ) : (a.log taylorDepth).mem_affine eps (Real.log v)

log is sound for positive inputs