Relaxation of optimization problems

We define the notion of relaxation. It is a reflexive and transitive relation and it induces a forward map between solutions. The idea is that solving the original problem is "as hard" as solving the relaxed problem. A strong equivalence gives a relaxation.

References

• [RelaxationWiki] https://en.wikipedia.org/wiki/Relaxation_(approximation)

structure Minimization.Relaxation {D : Type} {E : Type} {R : Type} [Preorder R] (p : Minimization D R) (q : Minimization E R) : Type

We read Relaxation p q as p relaxes to q or q is a relaxation of p.

• phi : D → E
• phi_feasibility : ∀ (x : D), p.feasible x → q.feasible (self.phi x)
• phi_optimality : ∀ (x : D), p.feasible x → q.objFun (self.phi x) ≤ p.objFun x

theorem Minimization.Relaxation.phi_feasibility {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.Relaxation q) (x : D) : p.feasible x → q.feasible (self.phi x)

theorem Minimization.Relaxation.phi_optimality {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (self : p.Relaxation q) (x : D) : p.feasible x → q.objFun (self.phi x) ≤ p.objFun x

def Minimization.Relaxation.«term_≽'_» : Lean.TrailingParserDescr

Equations

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

def Minimization.Relaxation.refl {D : Type} {R : Type} [Preorder R] {p : Minimization D R} : p.Relaxation p

Equations

• Minimization.Relaxation.refl = { phi := id, phi_feasibility := ⋯, phi_optimality := ⋯ }

def Minimization.Relaxation.trans {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} {r : Minimization F R} (Rx₁ : p.Relaxation q) (Rx₂ : q.Relaxation r) : p.Relaxation r

Equations

• Rx₁.trans Rx₂ = { phi := Rx₂.phi ∘ Rx₁.phi, phi_feasibility := ⋯, phi_optimality := ⋯ }

instance Minimization.Relaxation.instTrans {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] : Trans Minimization.Relaxation Minimization.Relaxation Minimization.Relaxation

Equations

• Minimization.Relaxation.instTrans = { trans := fun {a : Minimization D R} {b : Minimization E R} {c : Minimization F R} => Minimization.Relaxation.trans }

theorem Minimization.Relaxation.feasible_and_bounded_of_feasible {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (Rx : p.Relaxation q) {x : D} (h_feas_x : p.feasible x) : q.feasible (Rx.phi x) ∧ q.objFun (Rx.phi x) ≤ p.objFun x

First property in [RelaxationWiki].

theorem Minimization.Relaxation.induces_original_problem_optimality {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (Rx : p.Relaxation q) (phi_inv : E → D) (phi_left_inv : Function.LeftInverse Rx.phi phi_inv) (h_objFun : ∀ (x : D), p.feasible x → p.objFun x = q.objFun (Rx.phi x)) {y : E} (h_opt_y : q.optimal y) (h_feas_y : p.feasible (phi_inv y)) : p.optimal (phi_inv y)

Second property in [RelaxationWiki]. NOTE: This does not use Rx.phi_optimality.

def Minimization.Relaxation.ofStrongEquivalence {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E✝ R} (E : p.StrongEquivalence q) : p.Relaxation q

Equations

• Minimization.Relaxation.ofStrongEquivalence E = { phi := E.phi, phi_feasibility := ⋯, phi_optimality := ⋯ }

instance Minimization.Relaxation.instTransStrongEquivalence {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] : Trans Minimization.Relaxation Minimization.StrongEquivalence Minimization.Relaxation

Equations

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

instance Minimization.Relaxation.instTransStrongEquivalence_1 {D : Type} {E : Type} {F : Type} {R : Type} [Preorder R] : Trans Minimization.StrongEquivalence Minimization.Relaxation Minimization.Relaxation

Equations

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

def Minimization.StrongEquivalence.ofRelaxations {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (Rx₁ : p.Relaxation q) (Rx₂ : q.Relaxation p) : p.StrongEquivalence q

Equations

• Minimization.StrongEquivalence.ofRelaxations Rx₁ Rx₂ = { phi := Rx₁.phi, psi := Rx₂.phi, phi_feasibility := ⋯, psi_feasibility := ⋯, phi_optimality := ⋯, psi_optimality := ⋯ }

def Minimization.Equivalence.ofRelaxations {D : Type} {E : Type} {R : Type} [Preorder R] {p : Minimization D R} {q : Minimization E R} (Rx₁ : p.Relaxation q) (Rx₂ : q.Relaxation p) : p.Equivalence q

Equations

• Minimization.Equivalence.ofRelaxations Rx₁ Rx₂ = Minimization.Equivalence.ofStrongEquivalence (Minimization.StrongEquivalence.ofRelaxations Rx₁ Rx₂)

def Minimization.Relaxation.remove_constraint {D : Type} {R : Type} [Preorder R] {f : D → R} {cs : D → Prop} {c : D → Prop} {cs' : D → Prop} (hcs : ∀ (x : D), cs x ↔ c x ∧ cs' x) : { objFun := f, constraints := cs }.Relaxation { objFun := f, constraints := cs' }

Equations

• Minimization.Relaxation.remove_constraint hcs = { phi := id, phi_feasibility := ⋯, phi_optimality := ⋯ }

def Minimization.Relaxation.weaken_constraints {D : Type} {R : Type} [Preorder R] {f : D → R} {cs : D → Prop} (cs' : D → Prop) (hcs : ∀ (x : D), cs x → cs' x) : { objFun := f, constraints := cs }.Relaxation { objFun := f, constraints := cs' }

Equations

• Minimization.Relaxation.weaken_constraints cs' hcs = { phi := id, phi_feasibility := ⋯, phi_optimality := ⋯ }