§2.2, proof of Proposition 2.1(i), p. 5 — the feasible set of (P_𝒰) is contained in that of every instance

Proved

RobustUncLP.WorstCase.robustFeas_subset_instFeas

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-programmingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1robust-optimization

Let $\mathcal U$ be a set of real $m\times n$ matrices and $f\in\mathbb R^{n}$ . For every $A \in \mathcal U$ ,

G_{\mathcal U} = \{x \mid Bx \ge 0\ \forall B\in\mathcal U;\ f^{T}x = 1\} \ \subseteq\ \{x \mid Ax \ge 0,\ f^{T}x = 1\}.

This is the "if" part of Proposition 2.1(i): an infeasible instance makes the robust counterpart infeasible.

Preamble

import Mathlib
import Definitions.Def_RobustUncLP_WorstCase_Setting
open Matrix

Formal statement

namespace RobustUncLP.WorstCase

theorem robustFeas_subset_instFeas {m n : ℕ} (U : Set (Matrix (Fin m) (Fin n) ℝ))
    (f : Fin n → ℝ) :
    ∀ A ∈ U, robustFeas U f ⊆ instFeas f A := by sorry

end RobustUncLP.WorstCase

Source

Ben-Tal & Nemirovski, Robust solutions of uncertain linear programs, Oper. Res. Lett. 25 (1999); authors' manuscript, p. 5, §2.2, proof of Proposition 2.1, first sentence

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph