Global Optimization via Branch-and-Bound

This file implements verified global optimization over intervals using branch-and-bound with interval arithmetic and derivative bounds.

Phase Status

This module is now largely Phase 1 (verified). The core correctness theorems are fully proved for the ExprSupported subset.

Main definitions

• minimizeInterval - Find a lower bound on min f over an interval
• maximizeInterval - Find an upper bound on max f over an interval
• Correctness theorems (fully proved for ExprSupported)

Algorithm

Branch-and-bound with the following pruning rules:

1. Interval evaluation: If f([a,b]) = [lo, hi], then min f ≥ lo
2. Monotonicity: If f'([a,b]) > 0, f is increasing, so min is at a
3. Subdivision: Split interval and recurse

Optimization result

structure LeanCert.Engine.OptResult : Type

Result of an optimization computation

• valueBound : Core.IntervalRat

  Interval containing the optimum value

• argBound : Option Core.IntervalRat

  Interval containing an optimizing point (if found)

• depth : ℕ

  Depth of search performed

Minimization

noncomputable def LeanCert.Engine.derivStrictlyPositive (e : Core.Expr) (I : Core.IntervalRat) (varIdx : ℕ) : Bool

Check if derivative interval is strictly positive

Equations

• LeanCert.Engine.derivStrictlyPositive e I varIdx = decide (0 < (LeanCert.Engine.derivInterval e (fun (x : ℕ) => I) varIdx).lo)

noncomputable def LeanCert.Engine.derivStrictlyNegative (e : Core.Expr) (I : Core.IntervalRat) (varIdx : ℕ) : Bool

Check if derivative interval is strictly negative

Equations

• LeanCert.Engine.derivStrictlyNegative e I varIdx = decide ((LeanCert.Engine.derivInterval e (fun (x : ℕ) => I) varIdx).hi < 0)

noncomputable def LeanCert.Engine.minimizeInterval (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) : OptResult

Simple branch-and-bound minimization.

Returns an interval [lo, hi] such that:

• lo ≤ min_{x ∈ I} f(x)
• hi ≥ min_{x ∈ I} f(x)

Equations

• LeanCert.Engine.minimizeInterval e I varIdx maxDepth = LeanCert.Engine.minimizeInterval.go e varIdx maxDepth I maxDepth

@[irreducible]

noncomputable def LeanCert.Engine.minimizeInterval.go (e : Core.Expr) (varIdx maxDepth : ℕ) (J : Core.IntervalRat) (depth : ℕ) : OptResult

Equations

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

theorem LeanCert.Engine.minimizeInterval_base_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (x : ℝ) : x ∈ I → ↑(evalInterval1 e I).lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Base case correctness: interval evaluation gives a valid lower bound. This theorem is FULLY PROVED - no sorry, no axioms.

Derivative bounds and monotonicity

theorem LeanCert.Engine.derivInterval_correct_evalWithDeriv1 (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : deriv (evalFunc1 e) x ∈ (evalWithDeriv1 e I).der

For single-variable expressions evaluated with (fun _ => I), derivative is correct. We use evalWithDeriv1 which directly uses varActive for all variables.

theorem LeanCert.Engine.derivInterval_correct_single (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : deriv (evalFunc1 e) x ∈ derivInterval e (fun (x : ℕ) => I) 0

Derivative is in derivInterval for expressions that only use var 0. FULLY PROVED - no sorry.

theorem LeanCert.Engine.deriv_pos_on_interval (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) (x : ℝ) : x ∈ I → 0 < deriv (evalFunc1 e) x

If the derivative interval is strictly positive, derivative is positive everywhere

theorem LeanCert.Engine.deriv_neg_on_interval (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) (x : ℝ) : x ∈ I → deriv (evalFunc1 e) x < 0

If the derivative interval is strictly negative, derivative is negative everywhere

theorem LeanCert.Engine.strictMonoOn_of_deriv_pos_interval (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) : StrictMonoOn (evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)

Strictly positive derivative implies strict monotonicity

theorem LeanCert.Engine.strictAntiOn_of_deriv_neg_interval (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) : StrictAntiOn (evalFunc1 e) (Set.Icc ↑I.lo ↑I.hi)

Strictly negative derivative implies strict antitonicity

Monotonicity-based bounds

theorem LeanCert.Engine.increasing_min_at_left (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) (x : ℝ) : x ∈ I → evalFunc1 e ↑I.lo ≤ evalFunc1 e x

For increasing functions, minimum is at the left endpoint

theorem LeanCert.Engine.decreasing_min_at_right (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) (x : ℝ) : x ∈ I → evalFunc1 e ↑I.hi ≤ evalFunc1 e x

For decreasing functions, minimum is at the right endpoint

theorem LeanCert.Engine.increasing_endpoint_bound (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hpos : 0 < (derivInterval e (fun (x : ℕ) => I) 0).lo) (x : ℝ) : x ∈ I → ↑(evalInterval1 e (Core.IntervalRat.singleton I.lo)).lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Interval at left endpoint gives valid lower bound for increasing functions

theorem LeanCert.Engine.decreasing_endpoint_bound (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (hneg : (derivInterval e (fun (x : ℕ) => I) 0).hi < 0) (x : ℝ) : x ∈ I → ↑(evalInterval1 e (Core.IntervalRat.singleton I.hi)).lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Interval at right endpoint gives valid lower bound for decreasing functions

Full optimization correctness

theorem LeanCert.Engine.mem_bisect_cases (I : Core.IntervalRat) (x : ℝ) (hx : x ∈ I) : x ∈ I.bisect.1 ∨ x ∈ I.bisect.2

Helper: membership in bisected intervals

theorem LeanCert.Engine.minimizeInterval_go_correct (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (maxDepth depth : ℕ) (J : Core.IntervalRat) (x : ℝ) : x ∈ J → ↑(minimizeInterval.go e 0 maxDepth J depth).valueBound.lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Helper lemma for go correctness. FULLY PROVED for varIdx = 0 and UsesOnlyVar0 expressions.

theorem LeanCert.Engine.minimizeInterval_correct (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (maxDepth : ℕ) (x : ℝ) : x ∈ I → ↑(minimizeInterval e I 0 maxDepth).valueBound.lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Correctness: the minimum is in the computed interval. FULLY PROVED for varIdx = 0 and UsesOnlyVar0 expressions.

Maximization

noncomputable def LeanCert.Engine.maximizeInterval (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) : OptResult

Maximize by minimizing the negation

Equations

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

theorem LeanCert.Engine.maximizeInterval_correct (e : Core.Expr) (hsupp : ExprSupported e) (hvar0 : UsesOnlyVar0 e) (I : Core.IntervalRat) (maxDepth : ℕ) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑(maximizeInterval e I 0 maxDepth).valueBound.hi

Correctness: the maximum is in the computed interval. FULLY PROVED for varIdx = 0 and UsesOnlyVar0 expressions.

Bounds checking

noncomputable def LeanCert.Engine.checkLowerBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (varIdx maxDepth : ℕ) : Bool

Check if f(x) ≥ c for all x in I

Equations

• LeanCert.Engine.checkLowerBound e I c varIdx maxDepth = decide (c ≤ (LeanCert.Engine.minimizeInterval e I varIdx maxDepth).valueBound.lo)

noncomputable def LeanCert.Engine.checkUpperBound (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (varIdx maxDepth : ℕ) : Bool

Check if f(x) ≤ c for all x in I

Equations

• LeanCert.Engine.checkUpperBound e I c varIdx maxDepth = decide ((LeanCert.Engine.maximizeInterval e I varIdx maxDepth).valueBound.hi ≤ c)

N-Variable Optimization Infrastructure

The following section provides generalized optimization infrastructure that works with arbitrary variable indices and multi-variable environments. This allows optimizing along any coordinate while holding other variables fixed.

Key types:

• IntervalEnv := Nat → IntervalRat - maps variable indices to intervals
• evalAlong e ρ idx - evaluates e as a function of variable idx

The main advantage is that we can now optimize expressions with multiple variables by fixing all but one variable and optimizing along that coordinate.

N-variable derivative bounds

theorem LeanCert.Engine.deriv_pos_on_interval_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hpos : 0 < (derivInterval e ρ_int idx).lo) (x : ℝ) : x ∈ ρ_int idx → 0 < deriv (e.evalAlong ρ_real idx) x

If the derivative interval along idx is strictly positive, derivative is positive everywhere. Generalized version that works with any variable index and environment.

theorem LeanCert.Engine.deriv_neg_on_interval_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hneg : (derivInterval e ρ_int idx).hi < 0) (x : ℝ) : x ∈ ρ_int idx → deriv (e.evalAlong ρ_real idx) x < 0

If the derivative interval along idx is strictly negative, derivative is negative everywhere. Generalized version that works with any variable index and environment.

theorem LeanCert.Engine.strictMonoOn_of_deriv_pos_interval_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hpos : 0 < (derivInterval e ρ_int idx).lo) : StrictMonoOn (e.evalAlong ρ_real idx) (Set.Icc ↑(ρ_int idx).lo ↑(ρ_int idx).hi)

Strictly positive derivative along idx implies strict monotonicity. Generalized n-variable version.

theorem LeanCert.Engine.strictAntiOn_of_deriv_neg_interval_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hneg : (derivInterval e ρ_int idx).hi < 0) : StrictAntiOn (e.evalAlong ρ_real idx) (Set.Icc ↑(ρ_int idx).lo ↑(ρ_int idx).hi)

Strictly negative derivative along idx implies strict antitonicity. Generalized n-variable version.

N-variable monotonicity-based bounds

theorem LeanCert.Engine.increasing_min_at_left_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hpos : 0 < (derivInterval e ρ_int idx).lo) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).lo ≤ e.evalAlong ρ_real idx x

For increasing functions along idx, minimum is at the left endpoint. Generalized n-variable version.

theorem LeanCert.Engine.decreasing_min_at_right_idx (e : Core.Expr) (hsupp : ExprSupported e) (ρ_real : ℕ → ℝ) (ρ_int : IntervalEnv) (idx : ℕ) (hρ : ∀ (i : ℕ), ρ_real i ∈ ρ_int i) (hneg : (derivInterval e ρ_int idx).hi < 0) (x : ℝ) : x ∈ ρ_int idx → e.evalAlong ρ_real idx ↑(ρ_int idx).hi ≤ e.evalAlong ρ_real idx x

For decreasing functions along idx, minimum is at the right endpoint. Generalized n-variable version.

N-variable minimization algorithm

noncomputable def LeanCert.Engine.derivStrictlyPositive_idx (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) : Bool

Check if derivative interval along idx is strictly positive

Equations

• LeanCert.Engine.derivStrictlyPositive_idx e ρ idx = decide (0 < (LeanCert.Engine.derivInterval e ρ idx).lo)

noncomputable def LeanCert.Engine.derivStrictlyNegative_idx (e : Core.Expr) (ρ : IntervalEnv) (idx : ℕ) : Bool

Check if derivative interval along idx is strictly negative

Equations

• LeanCert.Engine.derivStrictlyNegative_idx e ρ idx = decide ((LeanCert.Engine.derivInterval e ρ idx).hi < 0)

def LeanCert.Engine.updateIntervalEnv (ρ : IntervalEnv) (idx : ℕ) (J : Core.IntervalRat) : IntervalEnv

Update an interval environment at a specific index

Equations

• LeanCert.Engine.updateIntervalEnv ρ idx J i = if i = idx then J else ρ i

noncomputable def LeanCert.Engine.minimizeIntervalIdx (e : Core.Expr) (ρ : IntervalEnv) (idx maxDepth : ℕ) : OptResult

N-variable branch-and-bound minimization along coordinate idx.

Returns an interval [lo, hi] such that for any ρ_real with ρ_real i ∈ ρ i:

• lo ≤ min_{t ∈ ρ idx} evalAlong e ρ_real idx t
• hi ≥ min_{t ∈ ρ idx} evalAlong e ρ_real idx t

Equations

• LeanCert.Engine.minimizeIntervalIdx e ρ idx maxDepth = LeanCert.Engine.minimizeIntervalIdx.go e ρ idx maxDepth (ρ idx) maxDepth

@[irreducible]

noncomputable def LeanCert.Engine.minimizeIntervalIdx.go (e : Core.Expr) (ρ : IntervalEnv) (idx maxDepth : ℕ) (J : Core.IntervalRat) (depth : ℕ) : OptResult

Equations

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

N-variable minimization correctness

theorem LeanCert.Engine.minimizeIntervalIdx_base_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ↑(evalInterval e ρ_int).lo ≤ Core.Expr.eval ρ_real e

Base case correctness for n-variable optimization. Interval evaluation gives a valid lower bound.

theorem LeanCert.Engine.mem_bisect_cases_idx (J : Core.IntervalRat) (t : ℝ) (ht : t ∈ J) : t ∈ J.bisect.1 ∨ t ∈ J.bisect.2

Helper: membership in bisected intervals

theorem LeanCert.Engine.minimizeIntervalIdx_go_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (idx maxDepth depth : ℕ) (J : Core.IntervalRat) (hJ_sub : ∀ t ∈ J, t ∈ ρ_int idx) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ J, ↑(minimizeIntervalIdx.go e ρ_int idx maxDepth J depth).valueBound.lo ≤ Core.Expr.eval (ρ_real[idx ↦ t]) e

Helper lemma for go correctness in n-variable setting

theorem LeanCert.Engine.minimizeIntervalIdx_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (idx maxDepth : ℕ) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ ρ_int idx, ↑(minimizeIntervalIdx e ρ_int idx maxDepth).valueBound.lo ≤ Core.Expr.eval (ρ_real[idx ↦ t]) e

Correctness theorem for n-variable minimization: For any real environment ρ_real satisfying ρ_int, and any t in ρ_int idx, the computed lower bound is valid.

FULLY PROVED - no sorry, no axioms.

noncomputable def LeanCert.Engine.maximizeIntervalIdx (e : Core.Expr) (ρ : IntervalEnv) (idx maxDepth : ℕ) : OptResult

N-variable maximization via minimization of negation

Equations

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

theorem LeanCert.Engine.maximizeIntervalIdx_correct (e : Core.Expr) (hsupp : ExprSupported e) (ρ_int : IntervalEnv) (idx maxDepth : ℕ) (ρ_real : ℕ → ℝ) : (∀ (i : ℕ), ρ_real i ∈ ρ_int i) → ∀ t ∈ ρ_int idx, Core.Expr.eval (ρ_real[idx ↦ t]) e ≤ ↑(maximizeIntervalIdx e ρ_int idx maxDepth).valueBound.hi

Correctness theorem for n-variable maximization

Backward-compatible wrappers

noncomputable def LeanCert.Engine.minimizeInterval' (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) : OptResult

Alternative single-variable minimization as a thin wrapper around minimizeIntervalIdx. This is equivalent to the original minimizeInterval but uses the generalized n-variable implementation.

Equations

• LeanCert.Engine.minimizeInterval' e I varIdx maxDepth = LeanCert.Engine.minimizeIntervalIdx e (fun (x : ℕ) => I) varIdx maxDepth

theorem LeanCert.Engine.minimizeInterval'_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) (x : ℝ) : x ∈ I → ↑(minimizeInterval' e I varIdx maxDepth).valueBound.lo ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Correctness theorem for single-variable minimization via the idx API. This doesn't require UsesOnlyVar0 - works for any expression.

noncomputable def LeanCert.Engine.maximizeInterval' (e : Core.Expr) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) : OptResult

Alternative maximization as a thin wrapper around maximizeIntervalIdx.

Equations

• LeanCert.Engine.maximizeInterval' e I varIdx maxDepth = LeanCert.Engine.maximizeIntervalIdx e (fun (x : ℕ) => I) varIdx maxDepth

theorem LeanCert.Engine.maximizeInterval'_correct (e : Core.Expr) (hsupp : ExprSupported e) (I : Core.IntervalRat) (varIdx maxDepth : ℕ) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑(maximizeInterval' e I varIdx maxDepth).valueBound.hi

Correctness theorem for single-variable maximization via the idx API.