Domain-aware automatic differentiation with Dyadic intervals

This module is the bounded-denominator counterpart of AD.DomainChecked. Polynomial dual arithmetic is performed with Dyadic endpoints and outward rounding after every addition and multiplication. Transcendental values use the same verified rational Taylor kernels as the Dyadic value evaluator and are rounded back to Dyadic endpoints.

The public entry points are checked: unsupported syntax, invalid reciprocal or logarithm domains, and positive rounding precisions return EvalError rather than a finite interval.

structure LeanCert.Engine.DualIntervalDyadic : Type

A value interval and one directional derivative interval, both Dyadic.

• val : Core.IntervalDyadic
• der : Core.IntervalDyadic

def LeanCert.Engine.instReprDualIntervalDyadic.repr : DualIntervalDyadic → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Engine.instReprDualIntervalDyadic : Repr DualIntervalDyadic

Equations

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

@[instance_reducible]

instance LeanCert.Engine.instInhabitedDualIntervalDyadic : Inhabited DualIntervalDyadic

Equations

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

@[reducible, inline]

abbrev LeanCert.Engine.DualDyadicEnv : Type

An environment of Dyadic dual intervals.

Equations

• LeanCert.Engine.DualDyadicEnv = (ℕ → LeanCert.Engine.DualIntervalDyadic)

def LeanCert.Engine.DualIntervalDyadic.const (q : ℚ) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

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

def LeanCert.Engine.DualIntervalDyadic.varActive (I : Core.IntervalDyadic) : DualIntervalDyadic

Equations

• LeanCert.Engine.DualIntervalDyadic.varActive I = { val := I, der := LeanCert.Engine.DualIntervalDyadic.one✝ }

def LeanCert.Engine.DualIntervalDyadic.varPassive (I : Core.IntervalDyadic) : DualIntervalDyadic

Equations

• LeanCert.Engine.DualIntervalDyadic.varPassive I = { val := I, der := LeanCert.Engine.DualIntervalDyadic.zero✝ }

def LeanCert.Engine.DualIntervalDyadic.add (a b : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

• a.add b cfg = { val := a.val.addRounded b.val cfg.precision, der := a.der.addRounded b.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.mul (a b : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

• a.mul b cfg = { val := a.val.mulRounded b.val cfg.precision, der := (a.der.mulRounded b.val cfg.precision).addRounded (a.val.mulRounded b.der cfg.precision) cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.neg (a : DualIntervalDyadic) : DualIntervalDyadic

Equations

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

def LeanCert.Engine.DualIntervalDyadic.inv (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

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

def LeanCert.Engine.DualIntervalDyadic.exp (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

• a.exp cfg = { val := LeanCert.Engine.expIntervalDyadic a.val cfg, der := (LeanCert.Engine.expIntervalDyadic a.val cfg).mulRounded a.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.sin (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

• a.sin cfg = { val := LeanCert.Engine.sinIntervalDyadic a.val cfg, der := (LeanCert.Engine.cosIntervalDyadic a.val cfg).mulRounded a.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.cos (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

• a.cos cfg = { val := LeanCert.Engine.cosIntervalDyadic a.val cfg, der := (LeanCert.Engine.sinIntervalDyadic a.val cfg).neg.mulRounded a.der cfg.precision }

def LeanCert.Engine.DualIntervalDyadic.log (a : DualIntervalDyadic) (cfg : DyadicConfig := { }) : DualIntervalDyadic

Equations

• a.log cfg = { val := LeanCert.Engine.logIntervalDyadic a.val cfg, der := (LeanCert.Engine.invIntervalDyadic a.val cfg).mulRounded a.der cfg.precision }

def LeanCert.Internal.AD.Dyadic.evalTotal (e : Core.Expr) (rho : Engine.DualDyadicEnv) (cfg : Engine.DyadicConfig := { }) : Engine.DualIntervalDyadic

Total computational kernel. Sound public use goes through the checked entry points below.

Equations

• LeanCert.Internal.AD.Dyadic.evalTotal (LeanCert.Core.Expr.const q) rho cfg = LeanCert.Engine.DualIntervalDyadic.const q cfg
• LeanCert.Internal.AD.Dyadic.evalTotal (LeanCert.Core.Expr.var i) rho cfg = rho i
• LeanCert.Internal.AD.Dyadic.evalTotal (a.add b) rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).add (LeanCert.Internal.AD.Dyadic.evalTotal b rho cfg) cfg
• LeanCert.Internal.AD.Dyadic.evalTotal (a.mul b) rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).mul (LeanCert.Internal.AD.Dyadic.evalTotal b rho cfg) cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.neg rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).neg
• LeanCert.Internal.AD.Dyadic.evalTotal a.inv rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).inv cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.exp rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).exp cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.sin rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).sin cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.cos rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).cos cfg
• LeanCert.Internal.AD.Dyadic.evalTotal a.log rho cfg = (LeanCert.Internal.AD.Dyadic.evalTotal a rho cfg).log cfg
• LeanCert.Internal.AD.Dyadic.evalTotal e rho cfg = default

def LeanCert.Engine.DualDyadicEnv.values (rho : DualDyadicEnv) : IntervalDyadicEnv

Value projection of a Dyadic dual environment.

Equations

• rho.values i = (rho i).val

def LeanCert.Engine.mkDualDyadicEnv (rho : IntervalDyadicEnv) (idx : ℕ) : DualDyadicEnv

Dual environment selecting coordinate idx.

Equations

• LeanCert.Engine.mkDualDyadicEnv rho idx i = if i = idx then LeanCert.Engine.DualIntervalDyadic.varActive (rho i) else LeanCert.Engine.DualIntervalDyadic.varPassive (rho i)

@[simp]

theorem LeanCert.Engine.mkDualDyadicEnv_values (rho : IntervalDyadicEnv) (idx : ℕ) : (mkDualDyadicEnv rho idx).values = rho

def LeanCert.Engine.checkDyadicADFragment : Core.Expr → Bool

The deliberately small v1 Dyadic AD fragment.

Equations

• LeanCert.Engine.checkDyadicADFragment (LeanCert.Core.Expr.const q) = true
• LeanCert.Engine.checkDyadicADFragment (LeanCert.Core.Expr.var i) = true
• LeanCert.Engine.checkDyadicADFragment (a.add b) = (LeanCert.Engine.checkDyadicADFragment a && LeanCert.Engine.checkDyadicADFragment b)
• LeanCert.Engine.checkDyadicADFragment (a.mul b) = (LeanCert.Engine.checkDyadicADFragment a && LeanCert.Engine.checkDyadicADFragment b)
• LeanCert.Engine.checkDyadicADFragment a.neg = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.inv = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.exp = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.sin = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.cos = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment a.log = LeanCert.Engine.checkDyadicADFragment a
• LeanCert.Engine.checkDyadicADFragment x✝ = false

def LeanCert.Engine.checkDyadicADDomain (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig := { }) : Bool

Box-dependent domain check for the Dyadic AD kernel.

Equations

• LeanCert.Engine.checkDyadicADDomain e rho cfg = (LeanCert.Engine.checkDyadicADFragment e && (LeanCert.Internal.Dyadic.evalCached e rho.values cfg).2)

def LeanCert.Engine.diagnoseDyadicADFailure (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig := { }) : EvalError

Explain the first failed support or domain check.

Equations

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

def LeanCert.Engine.evalDualDyadicChecked (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig := { }) : EvalResult DualIntervalDyadic

Checked Dyadic dual evaluation.

Equations

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

def LeanCert.Engine.evalWithDerivDyadicChecked (e : Core.Expr) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig := { }) : EvalResult DualIntervalDyadic

Checked value-and-derivative evaluation along coordinate idx.

Equations

• LeanCert.Engine.evalWithDerivDyadicChecked e rho idx cfg = LeanCert.Engine.evalDualDyadicChecked e (LeanCert.Engine.mkDualDyadicEnv rho idx) cfg

def LeanCert.Engine.derivIntervalDyadicChecked (e : Core.Expr) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Checked Dyadic derivative enclosure along coordinate idx.

Equations

• LeanCert.Engine.derivIntervalDyadicChecked e rho idx cfg = do let __do_lift ← LeanCert.Engine.evalWithDerivDyadicChecked e rho idx cfg pure __do_lift.der

def LeanCert.Engine.derivIntervalDyadicChecked1 (e : Core.Expr) (I : Core.IntervalDyadic) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Checked Dyadic derivative enclosure for a single-variable expression.

Equations

• LeanCert.Engine.derivIntervalDyadicChecked1 e I cfg = LeanCert.Engine.derivIntervalDyadicChecked e (fun (x : ℕ) => I) 0 cfg

def LeanCert.Engine.derivIntervalDyadicCheckedOfRat (e : Core.Expr) (rho : IntervalEnv) (idx : ℕ) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Convenience boundary for callers whose boxes use rational endpoints.

Equations

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

def LeanCert.Engine.derivIntervalDyadicChecked1OfRat (e : Core.Expr) (I : Core.IntervalRat) (cfg : DyadicConfig := { }) : EvalResult Core.IntervalDyadic

Single-variable rational-input convenience boundary.

Equations

• LeanCert.Engine.derivIntervalDyadicChecked1OfRat e I cfg = LeanCert.Engine.derivIntervalDyadicCheckedOfRat e (fun (x : ℕ) => I) 0 cfg

theorem LeanCert.Engine.evalTotalDyadic_val_of_fragment (e : Core.Expr) (rho : DualDyadicEnv) (cfg : DyadicConfig) (hsupp : checkDyadicADFragment e = true) : (Internal.AD.Dyadic.evalTotal e rho cfg).val = Internal.Dyadic.evalUnchecked e rho.values cfg

The value projection of the dual kernel is exactly the ordinary Dyadic value kernel.

theorem LeanCert.Engine.evalDualDyadicChecked_val_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : DualDyadicEnv) (cfg : DyadicConfig) (D : DualIntervalDyadic) (hrho : ∀ (i : ℕ), rhoReal i ∈ (rho i).val) (hok : evalDualDyadicChecked e rho cfg = Except.ok D) : Core.Expr.eval rhoReal e ∈ D.val

Golden theorem for successful checked Dyadic dual evaluation.

theorem LeanCert.Engine.evalWithDerivDyadicChecked_differentiableAt (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig) (D : DualIntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : evalWithDerivDyadicChecked e rho idx cfg = Except.ok D) : DifferentiableAt ℝ (e.evalAlong rhoReal idx) x

Successful checked Dyadic indexed AD proves differentiability throughout the selected input interval.

theorem LeanCert.Engine.evalWithDerivDyadicChecked_der_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig) (D : DualIntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : evalWithDerivDyadicChecked e rho idx cfg = Except.ok D) : deriv (e.evalAlong rhoReal idx) x ∈ D.der

Golden theorem: successful checked Dyadic indexed AD encloses the true partial derivative.

theorem LeanCert.Engine.derivIntervalDyadicChecked_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (idx : ℕ) (cfg : DyadicConfig) (dI : Core.IntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : derivIntervalDyadicChecked e rho idx cfg = Except.ok dI) : deriv (e.evalAlong rhoReal idx) x ∈ dI

Golden theorem for the derivative-only Dyadic API.

theorem LeanCert.Engine.derivIntervalDyadicCheckedOfRat_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalEnv) (idx : ℕ) (cfg : DyadicConfig) (dI : Core.IntervalDyadic) (x : ℝ) (hx : x ∈ rho idx) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (hok : derivIntervalDyadicCheckedOfRat e rho idx cfg = Except.ok dI) : deriv (e.evalAlong rhoReal idx) x ∈ dI

Golden theorem for rational input boxes converted to the Dyadic backend.

def LeanCert.Engine.gradientIntervalDyadicChecked (e : Core.Expr) (rho : IntervalDyadicEnv) (n : ℕ) (cfg : DyadicConfig := { }) : EvalResult (List Core.IntervalDyadic)

Compute the first n partial derivatives with the checked Dyadic backend.

Equations

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

def LeanCert.Engine.gradientIntervalDyadicCheckedOfRat (e : Core.Expr) (rho : IntervalEnv) (n : ℕ) (cfg : DyadicConfig := { }) : EvalResult (List Core.IntervalDyadic)

Rational-input convenience boundary for the first n Dyadic partials.

Equations

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

theorem LeanCert.Engine.gradientIntervalDyadicChecked_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalDyadicEnv) (n : ℕ) (cfg : DyadicConfig) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (gradient : List Core.IntervalDyadic) (hok : gradientIntervalDyadicChecked e rho n cfg = Except.ok gradient) : List.Forall₂ (fun (i : ℕ) (dI : Core.IntervalDyadic) => deriv (e.evalAlong rhoReal i) (rhoReal i) ∈ dI) (List.range n) gradient

Golden theorem for the checked Dyadic gradient API.

theorem LeanCert.Engine.gradientIntervalDyadicCheckedOfRat_correct (e : Core.Expr) (rhoReal : ℕ → ℝ) (rho : IntervalEnv) (n : ℕ) (cfg : DyadicConfig) (hrho : ∀ (i : ℕ), rhoReal i ∈ rho i) (gradient : List Core.IntervalDyadic) (hok : gradientIntervalDyadicCheckedOfRat e rho n cfg = Except.ok gradient) : List.Forall₂ (fun (i : ℕ) (dI : Core.IntervalDyadic) => deriv (e.evalAlong rhoReal i) (rhoReal i) ∈ dI) (List.range n) gradient

Golden theorem for checked Dyadic gradients over rational input boxes.