Automatic Differentiation - Basic Definitions

This file provides the core types and algebraic operations for forward-mode automatic differentiation using interval arithmetic.

Main definitions

• DualInterval - A pair of intervals representing (value, derivative)
• DualInterval.const - Constant dual (derivative is zero)
• DualInterval.varActive - Active variable (derivative is 1)
• DualInterval.varPassive - Passive variable (derivative is 0)
• DualInterval.add - Addition with sum rule
• DualInterval.mul - Multiplication with product rule
• DualInterval.neg - Negation

structure LeanCert.Engine.DualInterval : Type

Dual number with interval components: represents (value, derivative)

• val : Core.IntervalRat
• der : Core.IntervalRat

def LeanCert.Engine.instReprDualInterval.repr : DualInterval → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.instReprDualInterval : Repr DualInterval

Equations

• LeanCert.Engine.instReprDualInterval = { reprPrec := LeanCert.Engine.instReprDualInterval.repr }

instance LeanCert.Engine.instInhabitedDualInterval : Inhabited DualInterval

Default DualInterval for unsupported expression branches

Equations

• LeanCert.Engine.instInhabitedDualInterval = { default := { val := default, der := default } }

def LeanCert.Engine.DualInterval.const (q : ℚ) : DualInterval

Dual interval for a constant (derivative is zero)

Equations

• LeanCert.Engine.DualInterval.const q = { val := LeanCert.Core.IntervalRat.singleton q, der := LeanCert.Core.IntervalRat.singleton 0 }

def LeanCert.Engine.DualInterval.piConst : DualInterval

Dual interval for the constant π (derivative is zero)

Equations

• LeanCert.Engine.DualInterval.piConst = { val := LeanCert.Engine.piInterval, der := LeanCert.Core.IntervalRat.singleton 0 }

def LeanCert.Engine.DualInterval.varActive (I : Core.IntervalRat) : DualInterval

Dual interval for the variable we're differentiating with respect to

Equations

• LeanCert.Engine.DualInterval.varActive I = { val := I, der := LeanCert.Core.IntervalRat.singleton 1 }

def LeanCert.Engine.DualInterval.varPassive (I : Core.IntervalRat) : DualInterval

Dual interval for a passive variable

Equations

• LeanCert.Engine.DualInterval.varPassive I = { val := I, der := LeanCert.Core.IntervalRat.singleton 0 }

def LeanCert.Engine.DualInterval.add (d₁ d₂ : DualInterval) : DualInterval

Add two dual intervals

Equations

• d₁.add d₂ = { val := d₁.val.add d₂.val, der := d₁.der.add d₂.der }

def LeanCert.Engine.DualInterval.mul (d₁ d₂ : DualInterval) : DualInterval

Multiply two dual intervals (product rule)

Equations

• d₁.mul d₂ = { val := d₁.val.mul d₂.val, der := (d₁.der.mul d₂.val).add (d₁.val.mul d₂.der) }

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

Negate a dual interval

Equations

• d.neg = { val := d.val.neg, der := d.der.neg }

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

Inverse of a dual interval (quotient rule: d(1/f) = -f'/f²) Uses invInterval for the value component. For intervals containing zero, returns wide bounds.

Equations

• d.inv = { val := LeanCert.Engine.invInterval d.val, der := (d.der.mul ((LeanCert.Engine.invInterval d.val).mul (LeanCert.Engine.invInterval d.val))).neg }