Gradient Interval Computation for Optimization

This file provides functions to compute interval bounds on the gradient ∇f(B) of an expression over a box B. This is used for monotonicity-based pruning in branch-and-bound global optimization.

Main definitions

• gradientInterval - Compute interval bounds on all partial derivatives over a box
• gradientSignature - Determine the sign of each partial derivative
• canPruneToLo / canPruneToHi - Check if a coordinate can be pruned by monotonicity

Design

The gradient is computed by running forward-mode AD (from AD.lean) for each coordinate direction. The result is a list of intervals, one per variable.

Monotonicity pruning: If ∂f/∂xᵢ > 0 on the entire box B, then f is minimized when xᵢ = B[i].lo. We can shrink the box in that dimension to a point.

Gradient computation

noncomputable def LeanCert.Engine.Optimization.gradientInterval (e : Core.Expr) (B : Box) : List Core.IntervalRat

Compute the gradient interval: bounds on each partial derivative over a box. Returns a list of intervals, where the i-th interval contains ∂f/∂xᵢ for all x ∈ B.

Equations

• LeanCert.Engine.Optimization.gradientInterval e B = List.ofFn fun (i : Fin (List.length B)) => LeanCert.Engine.derivInterval e B.toEnv ↑i

noncomputable def LeanCert.Engine.Optimization.gradientIntervalN (e : Core.Expr) (B : Box) (n : ℕ) : List Core.IntervalRat

Compute gradient for n variables (explicit dimension)

Equations

• LeanCert.Engine.Optimization.gradientIntervalN e B n = List.map (fun (i : ℕ) => LeanCert.Engine.derivInterval e B.toEnv i) (List.range n)

Computable versions

def LeanCert.Engine.Optimization.mkDualEnvCore (ρ : IntervalEnv) (idx : ℕ) : DualEnv

Create dual environment for differentiating with respect to variable idx (computable). Active variable gets der = 1, passive variables get der = 0.

Equations

• LeanCert.Engine.Optimization.mkDualEnvCore ρ idx i = if i = idx then LeanCert.Engine.DualInterval.varActive (ρ i) else LeanCert.Engine.DualInterval.varPassive (ρ i)

def LeanCert.Engine.Optimization.evalWithDerivCore (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) (cfg : EvalConfig := { }) : DualInterval

Evaluate with derivative with respect to variable idx (computable version)

Equations

• LeanCert.Engine.Optimization.evalWithDerivCore e ρ idx cfg = LeanCert.Internal.AD.evalTotalCore e (LeanCert.Engine.Optimization.mkDualEnvCore ρ idx) cfg

def LeanCert.Engine.Optimization.derivIntervalCoreN (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) (cfg : EvalConfig := { }) : Core.IntervalRat

Computable derivative interval for multi-variable expressions. Computes the interval containing ∂f/∂xᵢ over the box.

Equations

• LeanCert.Engine.Optimization.derivIntervalCoreN e ρ idx cfg = (LeanCert.Engine.Optimization.evalWithDerivCore e ρ idx cfg).der

theorem LeanCert.Engine.Optimization.evalDualTotalCore_der_correct_idx (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (x : ℝ) (hx : x ∈ ρ_int idx) (cfg : EvalConfig) : deriv (e.evalAlong ρ_real idx) x ∈ (Internal.AD.evalTotalCore e (mkDualEnvCore ρ_int idx) cfg).der

Correctness of the computable derivative evaluator for an arbitrary coordinate of a multivariate expression.

def LeanCert.Engine.Optimization.gradientIntervalCore (e : Core.Expr) (B : Box) (cfg : EvalConfig := { }) : List Core.IntervalRat

Computable version of gradient interval for Core expressions. This can be used with native_decide for verified optimization.

Equations

• LeanCert.Engine.Optimization.gradientIntervalCore e B cfg = List.map (fun (i : ℕ) => LeanCert.Engine.Optimization.derivIntervalCoreN e B.toEnv i cfg) (List.range (List.length B))

def LeanCert.Engine.Optimization.gradientIntervalChecked (e : Core.Expr) (B : Box) (cfg : EvalConfig := { }) : EvalResult (List Core.IntervalRat)

Compute every partial derivative using the domain-aware checked AD path. Unlike gradientIntervalCore, this rejects unsupported syntax, reciprocal arguments containing zero, and nonpositive logarithm arguments instead of returning a finite interval that could be mistaken for a certificate.

Equations

• LeanCert.Engine.Optimization.gradientIntervalChecked e B cfg = List.mapM (fun (i : ℕ) => LeanCert.Engine.derivIntervalChecked e B.toEnv i cfg) (List.range (List.length B))

theorem LeanCert.Engine.Optimization.gradientIntervalChecked_correct (e : Core.Expr) (B : Box) (cfg : EvalConfig) (ρReal : ℕ → ℝ) (hρ : Box.envMem ρReal B) (hzero : ∀ i ≥ List.length B, ρReal i = 0) (gradient : List Core.IntervalRat) (hok : gradientIntervalChecked e B cfg = Except.ok gradient) : List.Forall₂ (fun (i : ℕ) (dI : Core.IntervalRat) => deriv (e.evalAlong ρReal i) (ρReal i) ∈ dI) (List.range (List.length B)) gradient

Golden soundness theorem for a successfully computed checked gradient. The output list is aligned with coordinates 0, …, B.length - 1.

Sign classification

inductive LeanCert.Engine.Optimization.IntervalSign : Type

Classification of an interval's sign

• positive : IntervalSign
• negative : IntervalSign
• nonpositive : IntervalSign
• nonnegative : IntervalSign
• indefinite : IntervalSign

def LeanCert.Engine.Optimization.instReprIntervalSign.repr : IntervalSign → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanCert.Engine.Optimization.instReprIntervalSign : Repr IntervalSign

Equations

• LeanCert.Engine.Optimization.instReprIntervalSign = { reprPrec := LeanCert.Engine.Optimization.instReprIntervalSign.repr }

@[instance_reducible]

instance LeanCert.Engine.Optimization.instDecidableEqIntervalSign : DecidableEq IntervalSign

Equations

• LeanCert.Engine.Optimization.instDecidableEqIntervalSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanCert.Engine.Optimization.classifySign (I : Core.IntervalRat) : IntervalSign

Classify the sign of an interval

Equations

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

noncomputable def LeanCert.Engine.Optimization.gradientSignature (e : Core.Expr) (B : Box) : List IntervalSign

The gradient signature: sign of each partial derivative (noncomputable wrapper)

Equations

• LeanCert.Engine.Optimization.gradientSignature e B = List.map LeanCert.Engine.Optimization.classifySign (LeanCert.Engine.Optimization.gradientIntervalN e B (List.length B))

Monotonicity predicates

def LeanCert.Engine.Optimization.isStrictlyPositive (I : Core.IntervalRat) : Bool

Check if interval is strictly positive

Equations

• LeanCert.Engine.Optimization.isStrictlyPositive I = decide (I.lo > 0)

def LeanCert.Engine.Optimization.isStrictlyNegative (I : Core.IntervalRat) : Bool

Check if interval is strictly negative

Equations

• LeanCert.Engine.Optimization.isStrictlyNegative I = decide (I.hi < 0)

def LeanCert.Engine.Optimization.isNonnegative (I : Core.IntervalRat) : Bool

Check if interval is nonnegative

Equations

• LeanCert.Engine.Optimization.isNonnegative I = decide (I.lo ≥ 0)

def LeanCert.Engine.Optimization.isNonpositive (I : Core.IntervalRat) : Bool

Check if interval is nonpositive

Equations

• LeanCert.Engine.Optimization.isNonpositive I = decide (I.hi ≤ 0)

Pruning queries

def LeanCert.Engine.Optimization.canPruneToLo (deriv_i : Core.IntervalRat) : Bool

Can we prune coordinate i to its low endpoint for minimization? True if ∂f/∂xᵢ > 0 on B (f is increasing in xᵢ, so min is at lo).

Equations

• LeanCert.Engine.Optimization.canPruneToLo deriv_i = LeanCert.Engine.Optimization.isStrictlyPositive deriv_i

def LeanCert.Engine.Optimization.canPruneToHi (deriv_i : Core.IntervalRat) : Bool

Can we prune coordinate i to its high endpoint for minimization? True if ∂f/∂xᵢ < 0 on B (f is decreasing in xᵢ, so min is at hi).

Equations

• LeanCert.Engine.Optimization.canPruneToHi deriv_i = LeanCert.Engine.Optimization.isStrictlyNegative deriv_i

def LeanCert.Engine.Optimization.pruneBoxForMin (B : Box) (grad : List Core.IntervalRat) : Box × List ℕ

Prune a box for minimization by fixing monotonic coordinates. Returns a (potentially smaller) box and a list of fixed coordinates.

Equations

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

Correctness theorems

theorem LeanCert.Engine.Optimization.gradientInterval_correct (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (ρ : ℕ → ℝ) (hρ : Box.envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) (i : Fin (List.length B)) : deriv (e.evalAlong ρ ↑i) (ρ ↑i) ∈ (gradientIntervalN e B (List.length B))[↑i]?.getD default

The computed gradient interval contains the true partial derivatives. This follows from evalDual_der_correct_idx in AD.lean.

theorem LeanCert.Engine.Optimization.pruneToLo_preserves_min (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (i : Fin (List.length B)) (hgrad : isStrictlyPositive (derivInterval e B.toEnv ↑i) = true) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ j ≥ List.length B, ρ j = 0) → ∃ (ρ' : ℕ → ℝ), Box.envMem ρ' B ∧ (∀ j ≥ List.length B, ρ' j = 0) ∧ ρ' ↑i = ↑B[↑i].lo ∧ Core.Expr.eval ρ' e ≤ Core.Expr.eval ρ e

If we prune a coordinate to lo because ∂f/∂xᵢ > 0, the minimum is preserved. Informal: if f is increasing in xᵢ on B, then min{f(x) : x ∈ B} = min{f(x) : xᵢ = B[i].lo}. NOTE: Requires ρ j = 0 for j ≥ B.length (standard assumption for box membership).

theorem LeanCert.Engine.Optimization.pruneToHi_preserves_min (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (i : Fin (List.length B)) (hgrad : isStrictlyNegative (derivInterval e B.toEnv ↑i) = true) (ρ : ℕ → ℝ) : Box.envMem ρ B → (∀ j ≥ List.length B, ρ j = 0) → ∃ (ρ' : ℕ → ℝ), Box.envMem ρ' B ∧ (∀ j ≥ List.length B, ρ' j = 0) ∧ ρ' ↑i = ↑B[↑i].hi ∧ Core.Expr.eval ρ' e ≤ Core.Expr.eval ρ e

If we prune a coordinate to hi because ∂f/∂xᵢ < 0, the minimum is preserved. NOTE: Requires ρ j = 0 for j ≥ B.length (standard assumption for box membership).

Pruned box membership and correctness

theorem LeanCert.Engine.Optimization.pruneBoxForMin_subset (B : Box) (grad : List Core.IntervalRat) (ρ : ℕ → ℝ) : Box.envMem ρ (pruneBoxForMin B grad).1 → Box.envMem ρ B

Helper: membership in the pruned box implies membership in the original box. The pruned box only shrinks coordinates, never expands them.

theorem LeanCert.Engine.Optimization.pruneBoxForMin_length (B : Box) (grad : List Core.IntervalRat) : List.length (pruneBoxForMin B grad).1 = List.length B

The pruned box has the same length as the original box

theorem LeanCert.Engine.Optimization.increasing_min_at_left_idx_core (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (cfg : EvalConfig) (hpos : 0 < (derivIntervalCoreN e ρ_int idx cfg).lo) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).lo ≤ e.evalAlong ρ_real idx x

A positive computable derivative enclosure makes the objective increasing along the selected coordinate.

theorem LeanCert.Engine.Optimization.decreasing_min_at_right_idx_core (e : Core.Expr) (hsupp : ADSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (cfg : EvalConfig) (hneg : (derivIntervalCoreN e ρ_int idx cfg).hi < 0) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).hi ≤ e.evalAlong ρ_real idx x

A negative computable derivative enclosure makes the objective decreasing along the selected coordinate.

theorem LeanCert.Engine.Optimization.pruneBoxForMin_correct (e : Core.Expr) (hsupp : ADSupported e) (B : Box) (cfg : EvalConfig := { }) : have grad := gradientIntervalCore e B cfg; have B' := (pruneBoxForMin B grad).1; ∀ (ρ : ℕ → ℝ), Box.envMem ρ B → (∀ i ≥ List.length B, ρ i = 0) → ∃ (ρ' : ℕ → ℝ), Box.envMem ρ' B' ∧ (∀ i ≥ List.length B', ρ' i = 0) ∧ Core.Expr.eval ρ' e ≤ Core.Expr.eval ρ e

Main correctness theorem for pruneBoxForMin:

After pruning, for any point ρ in the original box B, there exists a point ρ' in the pruned box B' such that f(ρ') ≤ f(ρ).

This means the minimum over B can be found by searching only in B'.

The proof constructs ρ' by moving each coordinate to its endpoint when the gradient has a definite sign. For each coordinate:

• If ∂f/∂xᵢ > 0 on B, move xᵢ to B[i].lo (f is increasing, min at left)
• If ∂f/∂xᵢ < 0 on B, move xᵢ to B[i].hi (f is decreasing, min at right)
• Otherwise, keep xᵢ = ρ[i]

The proof then shows f(ρ') ≤ f(ρ) by induction on coordinates, using the monotonicity lemmas increasing_min_at_left_idx and decreasing_min_at_right_idx.