theorem
LagrangianProblem.inner_constraintVector_eq_sum
{Q : Type u}
{m : ℕ}
(problem : LagrangianProblem Q m)
(x : Q)
(l : EuclideanSpace ℝ (Fin m))
:
inner ℝ l (problem.constraintVector x) = ∑ j : Fin m, l.ofLp j * problem.constraints j x
Helper for Definition 3.44: the inner product with the constraint vector expands as the coordinatewise weighted sum of the scalar constraint values.
theorem
LagrangianProblem.lagrangian_eq_objective_add_sum
{Q : Type u}
{m : ℕ}
(problem : LagrangianProblem Q m)
(x : Q)
(l : EuclideanSpace ℝ (Fin m))
:
problem.lagrangian x l = problem.objective x + ∑ j : Fin m, l.ofLp j * problem.constraints j x
The Lagrangian evaluates to the objective plus the weighted sum of the constraint values.
theorem
LagrangianProblem.dualFunction_eq_sInf_range_lagrangian
{Q : Type u}
{m : ℕ}
(problem : LagrangianProblem Q m)
(l : EuclideanSpace ℝ (Fin m))
:
problem.dualFunction l = sInf (Set.range fun (x : Q) => ↑(problem.lagrangian x l))
The project records the textbook dual function as the extended-real infimum of the Lagrangian over the decision set.
theorem
LagrangianProblem.dualFunction_eq_bot_of_not_mem_dualDomain
{Q : Type u}
{m : ℕ}
(problem : LagrangianProblem Q m)
{l : EuclideanSpace ℝ (Fin m)}
(hl : l ∉ problem.dualDomain)
:
problem.dualFunction l = ⊥
Helper for Definition 3.44: multipliers outside the dual domain contribute the value ⊥ to
the dual function.
theorem
LagrangianProblem.dualFunction_image_nonnegativeOrthant_subset_insert_bot_dualFeasibleSet
{Q : Type u}
{m : ℕ}
(problem : LagrangianProblem Q m)
:
problem.dualFunction '' EuclideanSpace.nonnegativeOrthant m ⊆ insert ⊥ (problem.dualFunction '' problem.dualFeasibleSet)
Helper for Definition 3.44: every dual value attained on the nonnegative orthant is either
⊥ or already attained on the dual-feasible set.
theorem
LagrangianProblem.dualOptimalValue_eq_sSup_image_nonnegativeOrthant
{Q : Type u}
{m : ℕ}
(problem : LagrangianProblem Q m)
:
problem.dualOptimalValue = sSup (problem.dualFunction '' EuclideanSpace.nonnegativeOrthant m)
The dual optimal value is the supremum of the dual function over the nonnegative orthant.