Automatic Differentiation - Partial Correctness Theorems

This file proves the correctness of the partial dual evaluator evalDual? which handles expressions with inv, log, and other domain-restricted functions.

Main theorems

• evalDual?_val_correct - Value component is correct when evalDual? returns some
• evalDual?1_val_correct - Single-variable version
• evalFunc1_differentiableAt_of_evalDual? - Differentiability when evalDual? succeeds
• evalDual?_der_correct - Derivative component is correct
• evalDual?1_correct - Combined correctness theorem

Design notes

All theorems are FULLY PROVED with no sorry or axioms. The key insight is that when evalDual? returns some, the domain constraints (nonzero for inv, positive for log) are satisfied.

Correctness of partial dual evaluator

theorem LeanCert.Engine.evalDual?_val_correct (e : Core.Expr) (hsupp : ExprSupportedWithInv e) (ρ_real : ℕ → ℝ) (ρ_dual : DualEnv) (D : DualInterval) (hsome : evalDual? e ρ_dual = some D) (hρ : ∀ (i : ℕ), ρ_real i ∈ (ρ_dual i).val) : Core.Expr.eval ρ_real e ∈ D.val

The value component of evalDual? is correct when it returns some. This theorem extends to expressions with inv.

theorem LeanCert.Engine.evalDual?1_val_correct (e : Core.Expr) (hsupp : ExprSupportedWithInv e) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDual?1 e I = some D) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ D.val

Single-variable version of evalDual?_val_correct

theorem LeanCert.Engine.evalFunc1_inv (e : Core.Expr) : evalFunc1 e.inv = fun (t : ℝ) => (evalFunc1 e t)⁻¹

Helper lemma: evalFunc1 for inv unfolds correctly

theorem LeanCert.Engine.evalFunc1_differentiableAt_of_evalDual? (e : Core.Expr) (hsupp : ExprSupportedWithInv e) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDual?1 e I = some D) : DifferentiableAt ℝ (evalFunc1 e) x

Expressions with inv are differentiable when the denominator is nonzero.

theorem LeanCert.Engine.evalDual?_der_correct (e : Core.Expr) (hsupp : ExprSupportedWithInv e) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDual?1 e I = some D) : deriv (evalFunc1 e) x ∈ D.der

The derivative component of evalDual? is correct when it returns some. For a supported expression (with inv) evaluated at a point x in the interval I, the derivative of the expression lies in the computed derivative interval.

This extends the AD correctness theorem to expressions with inv.

theorem LeanCert.Engine.evalDual?1_correct (e : Core.Expr) (hsupp : ExprSupportedWithInv e) (I : Core.IntervalRat) (D : DualInterval) (x : ℝ) (hx : x ∈ I) (hsome : evalDual?1 e I = some D) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ∈ D.val ∧ deriv (evalFunc1 e) x ∈ D.der

Combined correctness theorem for evalDual?1