Automatic Differentiation - Transcendental Functions

This file provides dual interval implementations for transcendental functions, implementing the chain rule for each.

Main definitions

Total functions (always succeed)

• DualInterval.sin - Sine with chain rule
• DualInterval.cos - Cosine with chain rule
• DualInterval.exp - Exponential with chain rule
• DualInterval.atan - Arctangent with chain rule
• DualInterval.arsinh - Inverse hyperbolic sine
• DualInterval.sinh, cosh, tanh - Hyperbolic functions
• DualInterval.erf - Error function
• DualInterval.sqrt - Square root (conservative derivative bound)
• DualInterval.sinc - sinc function

Partial functions (return Option)

• DualInterval.atanh? - Inverse hyperbolic tangent (requires |x| < 1)
• DualInterval.inv? - Inverse (requires nonzero)
• DualInterval.log? - Logarithm (requires positive)
• DualInterval.sqrt? - Square root with tight bounds (requires positive)

def LeanCert.Engine.DualInterval.sin (d : DualInterval) : DualInterval

Dual for sin (chain rule: d(sin f) = cos(f) * f')

Equations

• d.sin = { val := LeanCert.Engine.sinInterval d.val, der := (LeanCert.Engine.cosInterval d.val).mul d.der }

def LeanCert.Engine.DualInterval.cos (d : DualInterval) : DualInterval

Dual for cos (chain rule: d(cos f) = -sin(f) * f')

Equations

• d.cos = { val := LeanCert.Engine.cosInterval d.val, der := (LeanCert.Engine.sinInterval d.val).neg.mul d.der }

noncomputable def LeanCert.Engine.DualInterval.exp (d : DualInterval) : DualInterval

Dual for exp (chain rule: d(exp f) = exp(f) * f')

Equations

• d.exp = { val := d.val.expInterval, der := d.val.expInterval.mul d.der }

def LeanCert.Engine.DualInterval.unitInterval : Core.IntervalRat

The interval [0, 1] used to bound derivative factors in (0, 1]

Equations

• LeanCert.Engine.DualInterval.unitInterval = { lo := 0, hi := 1, le := LeanCert.Engine.DualInterval.unitInterval._proof_1 }

theorem LeanCert.Engine.DualInterval.arctan_deriv_factor_mem_unitInterval (y : ℝ) : 1 / (1 + y ^ 2) ∈ unitInterval

The derivative factor for arctan: 1/(1+x²) is in [0, 1]

theorem LeanCert.Engine.DualInterval.arsinh_deriv_factor_mem_unitInterval (y : ℝ) : (√(1 + y ^ 2))⁻¹ ∈ unitInterval

The derivative factor for arsinh: 1/√(1+x²) is in [0, 1]

def LeanCert.Engine.DualInterval.atan (d : DualInterval) : DualInterval

Dual for atan (chain rule: d(atan f) = f' / (1 + f²))

Equations

• d.atan = { val := LeanCert.Engine.atanInterval d.val, der := d.der.mul LeanCert.Engine.DualInterval.unitInterval }

def LeanCert.Engine.DualInterval.arsinh (d : DualInterval) : DualInterval

Dual for arsinh (chain rule: d(arsinh f) = f' / √(1 + f²))

Equations

• d.arsinh = { val := LeanCert.Engine.arsinhInterval d.val, der := d.der.mul LeanCert.Engine.DualInterval.unitInterval }

def LeanCert.Engine.DualInterval.sinh (d : DualInterval) : DualInterval

Dual for sinh (chain rule: d(sinh f) = cosh(f) * f')

Equations

• d.sinh = { val := LeanCert.Engine.sinhInterval d.val, der := (LeanCert.Engine.coshInterval d.val).mul d.der }

def LeanCert.Engine.DualInterval.cosh (d : DualInterval) : DualInterval

Dual for cosh (chain rule: d(cosh f) = sinh(f) * f')

Equations

• d.cosh = { val := LeanCert.Engine.coshInterval d.val, der := (LeanCert.Engine.sinhInterval d.val).mul d.der }

def LeanCert.Engine.DualInterval.tanh (d : DualInterval) : DualInterval

Dual for tanh (chain rule: d(tanh f) = sech²(f) * f' = (1 - tanh²(f)) * f') Since sech²(x) = 1 - tanh²(x) ∈ (0, 1] for all x, we use [0, 1] as bound.

Equations

• d.tanh = { val := LeanCert.Engine.tanhInterval d.val, der := d.der.mul LeanCert.Engine.DualInterval.unitInterval }

def LeanCert.Engine.DualInterval.two_div_sqrt_pi : Core.IntervalRat

Interval containing 2/√π ≈ 1.128379...

Equations

• LeanCert.Engine.DualInterval.two_div_sqrt_pi = { lo := 1128 / 1000, hi := 1129 / 1000, le := LeanCert.Engine.DualInterval.two_div_sqrt_pi._proof_1 }

noncomputable def LeanCert.Engine.DualInterval.erf (d : DualInterval) : DualInterval

Dual for erf (chain rule: d(erf f) = (2/√π) * exp(-f²) * f') erf'(x) = (2/√π) * exp(-x²), which is always positive and bounded by 2/√π ≈ 1.13

Equations

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

def LeanCert.Engine.DualInterval.erfCore (d : DualInterval) (n : ℕ := 10) : DualInterval

Computable dual for erf using expComputable

Equations

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

def LeanCert.Engine.DualInterval.sqrt (d : DualInterval) : DualInterval

Dual for sqrt (chain rule: d(sqrt f) = f' / (2 * sqrt(f))) sqrt'(x) = 1/(2*sqrt(x)) for x > 0, undefined at x = 0. We use sqrtInterval for the value and a conservative bound for the derivative. Note: The derivative blows up as x → 0+, so this uses a wide conservative bound.

Equations

• d.sqrt = { val := d.val.sqrtInterval, der := d.der.mul { lo := -100, hi := 100, le := LeanCert.Engine.DualInterval.sqrt._proof_1 } }

def LeanCert.Engine.DualInterval.sincDerivBound : Core.IntervalRat

Conservative derivative bound [-1, 1] for sinc derivative

Equations

• LeanCert.Engine.DualInterval.sincDerivBound = { lo := -1, hi := 1, le := LeanCert.Engine.DualInterval.erf._proof_1 }

def LeanCert.Engine.DualInterval.sinc (d : DualInterval) : DualInterval

Dual for sinc (chain rule: d(sinc f) = sinc'(f) * f') sinc'(x) = (x cos x - sin x) / x² for x ≠ 0, limit 0 at x = 0. We use conservative bound: |sinc'(x)| ≤ 1 for all x.

Equations

• d.sinc = { val := { lo := -1, hi := 1, le := LeanCert.Engine.DualInterval.erf._proof_1 }, der := LeanCert.Engine.DualInterval.sincDerivBound.mul d.der }

Partial functions (domain-restricted)

noncomputable def LeanCert.Engine.DualInterval.atanh? (d : DualInterval) : Option DualInterval

Partial dual for atanh (chain rule: d(atanh f) = f' / (1 - f²)) Returns None if the value interval is not contained in (-1, 1).

Equations

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

def LeanCert.Engine.DualInterval.inv? (d : DualInterval) : Option DualInterval

Partial dual for inv (chain rule: d(1/f) = -f'/f²) Returns None if the value interval contains zero.

Equations

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

noncomputable def LeanCert.Engine.DualInterval.log? (d : DualInterval) : Option DualInterval

Partial dual for log (chain rule: d(log f) = f'/f) Returns None if the value interval is not strictly positive.

Equations

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

def LeanCert.Engine.DualInterval.sqrtDerivCoefBound (lo : ℚ) (hpos : 0 < lo) : Core.IntervalRat

Compute a conservative upper bound on 1/(2*sqrt(lo)) for lo > 0. Uses the fact that:

• For 0 < lo ≤ 1: sqrt(lo) ≥ lo, so 1/(2sqrt(lo)) ≤ 1/(2lo)
• For lo > 1: sqrt(lo) > 1, so 1/(2*sqrt(lo)) < 1/2

Equations

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

theorem LeanCert.Engine.DualInterval.sqrtDerivCoef_bound {x lo : ℝ} (hlo_pos : 0 < lo) (hx_ge : lo ≤ x) : 1 / (2 * √x) ≤ max (1 / (2 * lo)) (1 / 2)

For lo > 0, the derivative coefficient 1/(2*sqrt(x)) is bounded above for x ≥ lo.

noncomputable def LeanCert.Engine.DualInterval.sqrt? (d : DualInterval) : Option DualInterval

Partial dual for sqrt (chain rule: d(sqrt f) = f' / (2 * sqrt(f))) Returns None if the value interval is not strictly positive.

Equations

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