N-Dimensional Boxes for Global Optimization

This file provides the Box type for representing n-dimensional domains as products of intervals, along with helper functions for branch-and-bound optimization.

Main definitions

• Box - A list of intervals representing an n-dimensional box
• Box.toEnv - Convert a box to an interval environment
• Box.mem - Membership: a point (list of reals) is in a box
• Box.widestDim - Find the dimension with the largest width (for splitting)
• Box.split - Split a box along a given dimension
• Box.volume - Product of interval widths (heuristic measure)

Design

A Box is represented as List IntervalRat, where the i-th element is the interval for the i-th variable. This allows boxes of any dimension.

For expressions with n variables (var 0 through var n-1), a box should have at least n intervals. The conversion Box.toEnv returns default for out-of-bounds indices.

Box type and basic operations

@[reducible, inline]

abbrev LeanCert.Engine.Optimization.Box : Type

An n-dimensional box as a list of intervals. The i-th element is the interval for variable i.

Equations

• LeanCert.Engine.Optimization.Box = List LeanCert.Core.IntervalRat

@[reducible, inline]

abbrev LeanCert.Engine.Optimization.Point : Type

A point in ℝⁿ represented as a list of reals

Equations

• LeanCert.Engine.Optimization.Point = List ℝ

@[reducible, inline]

abbrev LeanCert.Engine.Optimization.PointQ : Type

A rational point in ℚⁿ

Equations

• LeanCert.Engine.Optimization.PointQ = List ℚ

def LeanCert.Engine.Optimization.Box.ofInterval (I : Core.IntervalRat) : Box

Create a one-dimensional box from a single interval.

Equations

• LeanCert.Engine.Optimization.Box.ofInterval I = [I]

def LeanCert.Engine.Optimization.Box.toEnv (B : Box) : IntervalEnv

Convert a box to an interval environment. Returns default for out-of-bounds indices (i.e., the whole real line approximation).

Equations

• B.toEnv i = List.getD B i default

def LeanCert.Engine.Optimization.Box.dim (B : Box) : ℕ

The dimension (number of intervals) of a box

Equations

• B.dim = List.length B

def LeanCert.Engine.Optimization.Box.mem (p : Point) (B : Box) : Prop

Check if a point is in a box. A point is in a box if each coordinate is in the corresponding interval.

Equations

• LeanCert.Engine.Optimization.Box.mem p B = ∃ (h : List.length p = List.length B), ∀ (i : Fin (List.length B)), p[↑i] ∈ B[↑i]

def LeanCert.Engine.Optimization.Box.envMem (ρ : ℕ → ℝ) (B : Box) : Prop

Membership for a real function (environment) in a box. This is the key notion for correctness: ρ ∈ B means ρ i ∈ B[i] for all i < B.length.

Equations

• LeanCert.Engine.Optimization.Box.envMem ρ B = ∀ (i : Fin (List.length B)), ρ ↑i ∈ B[↑i]

theorem LeanCert.Engine.Optimization.Box.envMem_toEnv (ρ : ℕ → ℝ) (B : Box) (h : envMem ρ B) (hzero : ∀ i ≥ List.length B, ρ i = 0) : Engine.envMem ρ B.toEnv

envMem implies the general IntervalEnv membership for toEnv NOTE: For indices beyond the box dimension, we use the default interval [0,0]. This means expressions should only use variables 0..B.length-1 for correct results.

Width and dimension selection

def LeanCert.Engine.Optimization.Box.intervalWidth (I : Core.IntervalRat) : ℚ

Width of an interval

Equations

• LeanCert.Engine.Optimization.Box.intervalWidth I = I.hi - I.lo

def LeanCert.Engine.Optimization.Box.widths (B : Box) : List ℚ

Get the width of each dimension

Equations

• B.widths = List.map LeanCert.Engine.Optimization.Box.intervalWidth B

def LeanCert.Engine.Optimization.Box.maxIdx (xs : List ℚ) : ℕ

Find the index of the maximum element in a list (returns 0 for empty list)

Equations

• One or more equations did not get rendered due to their size.
• LeanCert.Engine.Optimization.Box.maxIdx [] = 0
• LeanCert.Engine.Optimization.Box.maxIdx [head] = 0

def LeanCert.Engine.Optimization.Box.widestDim (B : Box) : ℕ

Find the dimension with the widest interval (heuristic for splitting). Returns 0 if the box is empty.

Equations

• B.widestDim = LeanCert.Engine.Optimization.Box.maxIdx B.widths

def LeanCert.Engine.Optimization.Box.widestDim' (B : Box) : ℕ

Alternative: find widest dimension with explicit fold

Equations

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

Box splitting

def LeanCert.Engine.Optimization.Box.split (B : Box) (dim : ℕ) : Box × Box

Split a box along a given dimension by bisecting that interval. Returns the original box if the dimension is out of bounds.

Equations

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

def LeanCert.Engine.Optimization.Box.splitWidest (B : Box) : Box × Box

Split along the widest dimension

Equations

• B.splitWidest = B.split B.widestDim

theorem LeanCert.Engine.Optimization.Box.split_length_eq (B : Box) (d : ℕ) : List.length (B.split d).1 = List.length B ∧ List.length (B.split d).2 = List.length B

Splitting preserves the number of box coordinates.

theorem LeanCert.Engine.Optimization.Box.envMem_of_envMem_split (B : Box) (d : ℕ) (ρ : ℕ → ℝ) : envMem ρ (B.split d).1 → envMem ρ B

The lower child of a split is a semantic sub-box of its parent.

theorem LeanCert.Engine.Optimization.Box.envMem_of_envMem_split_right (B : Box) (d : ℕ) (ρ : ℕ → ℝ) : envMem ρ (B.split d).2 → envMem ρ B

The upper child of a split is a semantic sub-box of its parent.

Volume and size heuristics

def LeanCert.Engine.Optimization.Box.volume (B : Box) : ℚ

Volume of a box (product of widths). Returns 0 for empty box.

Equations

• B.volume = List.foldl (fun (x1 x2 : ℚ) => x1 * x2) 1 B.widths

def LeanCert.Engine.Optimization.Box.maxWidth (B : Box) : ℚ

Maximum width across all dimensions

Equations

• B.maxWidth = List.foldl max 0 B.widths

def LeanCert.Engine.Optimization.Box.isSmall (B : Box) (threshold : ℚ) : Bool

Check if a box is "small" (max width below threshold)

Equations

• B.isSmall threshold = decide (B.maxWidth ≤ threshold)

Box construction helpers

def LeanCert.Engine.Optimization.Box.ofPairs (pairs : List (ℚ × ℚ)) : Box

Create a box from a list of (lo, hi) pairs

Equations

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

def LeanCert.Engine.Optimization.Box.unit (n : ℕ) : Box

Create a unit box [0,1]ⁿ

Equations

• LeanCert.Engine.Optimization.Box.unit n = List.replicate n { lo := 0, hi := 1, le := LeanCert.Engine.Optimization.Box.unit._proof_1 }

def LeanCert.Engine.Optimization.Box.symmetric (n : ℕ) : Box

Create a symmetric box [-1,1]ⁿ

Equations

• LeanCert.Engine.Optimization.Box.symmetric n = List.replicate n { lo := -1, hi := 1, le := LeanCert.Engine.Optimization.Box.symmetric._proof_1 }

def LeanCert.Engine.Optimization.Box.ofBounds (los his : List ℚ) (_h : los.length = his.length) : Box

Create a box from bounds: [lo₀, hi₀] × ... × [loₙ₋₁, hiₙ₋₁]

Equations

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

Membership lemmas

theorem LeanCert.Engine.Optimization.Box.coord_mem_of_mem (p : Point) (B : Box) (h : mem p B) (i : Fin (List.length B)) : p[↑i] ∈ B[↑i]

If a point is in a box, its i-th coordinate is in the i-th interval

theorem LeanCert.Engine.Optimization.Box.mem_split_cases (B : Box) (d : ℕ) (hd : d < List.length B) (p : Point) (hp : mem p B) : mem p (B.split d).1 ∨ mem p (B.split d).2

After splitting, any point in the original box is in one of the halves.

theorem LeanCert.Engine.Optimization.Box.envMem_split_cases (B : Box) (d : ℕ) (hd : d < List.length B) (ρ : ℕ → ℝ) (hρ : envMem ρ B) : envMem ρ (B.split d).1 ∨ envMem ρ (B.split d).2

Environment membership after splitting.