29.5 Projecting phase II back to the original program
The lock forces the artificial coordinate to zero. Therefore optimality and unboundedness of the phase-II program project directly to the original LP.
namespace CLRSnamespace Chapter29namespace StandardLPAn optimal locked-auxiliary assignment projects to an optimal original assignment.
theorem lockedAuxiliary_optimal_to_original (P : StandardLP m n)
{z : Fin (n + 1) → ℝ} (hz : P.lockedAuxiliary.IsOptimal z) :
P.IsOptimal (auxiliaryTail z) := by
have hzparts := (P.lockedAuxiliary_feasible_iff z).1 hz.1
refine ⟨hzparts.2, ?_⟩
intro x hx
let u := auxiliaryAssignment 0 x
have hu : P.lockedAuxiliary.IsFeasible u :=
(P.lockedAuxiliary_feasible_iff u).2 ⟨rfl, by simpa [u]⟩
have hle := hz.2 u hu
rw [P.lockedAuxiliary_objective u,
P.lockedAuxiliary_objective z] at hle
simpa [u] using hleAn unbounded locked-auxiliary program makes the original program unbounded.
theorem lockedAuxiliary_unbounded_to_original (P : StandardLP m n)
(h : P.lockedAuxiliary.IsUnbounded) : P.IsUnbounded := by
intro M
obtain ⟨z, hz, hlarge⟩ := h M
have hzparts := (P.lockedAuxiliary_feasible_iff z).1 hz
refine ⟨auxiliaryTail z, hzparts.2, ?_⟩
rw [← P.lockedAuxiliary_objective z]
exact hlargeend StandardLPend Chapter29end CLRS