Global Optimization Examples

This file demonstrates the branch-and-bound global optimization algorithm on multivariate expressions over n-dimensional boxes.

Examples

Univariate

• Minimize x² over [-1, 1] → global min at x = 0
• Minimize (x - 1/2)² over [0, 1] → global min at x = 1/2

Multivariate

• Minimize x² + y² over [-1, 1]² → global min at (0, 0)
• Rosenbrock function: (1 - x)² + 100(y - x²)² over [-2, 2]²
• Beale function on a box

Expression builders

def LeanCert.Examples.GlobalOptimization.exprXSq : Core.Expr

The expression x² (variable 0 squared)

Equations

• LeanCert.Examples.GlobalOptimization.exprXSq = (LeanCert.Core.Expr.var 0).mul (LeanCert.Core.Expr.var 0)

def LeanCert.Examples.GlobalOptimization.exprYSq : Core.Expr

The expression y² (variable 1 squared)

Equations

• LeanCert.Examples.GlobalOptimization.exprYSq = (LeanCert.Core.Expr.var 1).mul (LeanCert.Core.Expr.var 1)

def LeanCert.Examples.GlobalOptimization.exprSumSq : Core.Expr

The expression x² + y²

Equations

• LeanCert.Examples.GlobalOptimization.exprSumSq = LeanCert.Examples.GlobalOptimization.exprXSq.add LeanCert.Examples.GlobalOptimization.exprYSq

def LeanCert.Examples.GlobalOptimization.exprShiftedSq (c : ℚ) : Core.Expr

The expression (x - c)² for a constant c

Equations

• LeanCert.Examples.GlobalOptimization.exprShiftedSq c = ((LeanCert.Core.Expr.var 0).add (LeanCert.Core.Expr.const c).neg).mul ((LeanCert.Core.Expr.var 0).add (LeanCert.Core.Expr.const c).neg)

def LeanCert.Examples.GlobalOptimization.exprOneMinusXSq : Core.Expr

The expression (1 - x)²

Equations

• LeanCert.Examples.GlobalOptimization.exprOneMinusXSq = ((LeanCert.Core.Expr.const 1).add (LeanCert.Core.Expr.var 0).neg).mul ((LeanCert.Core.Expr.const 1).add (LeanCert.Core.Expr.var 0).neg)

def LeanCert.Examples.GlobalOptimization.exprYMinusXSqSq : Core.Expr

The expression (y - x²)²

Equations

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

def LeanCert.Examples.GlobalOptimization.exprRosenbrock : Core.Expr

Rosenbrock function: (1 - x)² + 100(y - x²)²

Equations

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

Box construction

def LeanCert.Examples.GlobalOptimization.boxUnit2D : Engine.Optimization.Box

Unit box [0, 1]²

Equations

• LeanCert.Examples.GlobalOptimization.boxUnit2D = LeanCert.Engine.Optimization.Box.unit 2

def LeanCert.Examples.GlobalOptimization.boxSym2D : Engine.Optimization.Box

Symmetric box [-1, 1]²

Equations

• LeanCert.Examples.GlobalOptimization.boxSym2D = LeanCert.Engine.Optimization.Box.symmetric 2

def LeanCert.Examples.GlobalOptimization.boxLarge2D : Engine.Optimization.Box

A larger box [-2, 2]² for Rosenbrock

Equations

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

Example evaluations

Box operations demo