Minimization and Solution

This file defines:

• Minimization: the type of optimization problems, which we assume to be minimization problems.
• Solution: the type representing the solution set for an optimization problem.

These are the building blocks of the rest of the library.

structure Minimization (D : Type) (R : Type) : Type

Type of an optimization problem.

• objFun : D → R
• constraints : D → Prop

@[reducible]

def Minimization.feasible {D : Type} {R : Type} (p : Minimization D R) (x : D) : Prop

A point x : D is feasible in p if it satisfies the constraints.

Equations

• p.feasible x = p.constraints x

@[reducible]

def Minimization.optimal {D : Type} {R : Type} [Preorder R] (p : Minimization D R) (x : D) : Prop

A point x : D is optimal in p if it is feasible and for any feasible point y : D the value of x is a lower bound to the value of y.

Equations

• p.optimal x = (p.feasible x ∧ ∀ (y : D), p.feasible y → p.objFun x ≤ p.objFun y)

structure Minimization.Solution {D : Type} {R : Type} [Preorder R] (p : Minimization D R) : Type

A solution is simply an optimal point.

• point : D
• isOptimal : p.optimal self.point

theorem Minimization.Solution.isOptimal {D : Type} {R : Type} [Preorder R] {p : Minimization D R} (self : p.Solution) : p.optimal self.point