Prove2Me

Sufficient condition for extending xx to a feasible solution of (RC): ∑jaijxj+ϵβi(x)≤bi+\sum_ja_{ij}x_j+\epsilon\beta_i(x)\le b_i^+

Proved
RobustLP.Counterpart.rc_extension_of_beta

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

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

Let an uncertain linear program with uncertain-entry sets JiJ_i be given, and let ϵ>0\epsilon>0, δ>0\delta>0, Ω>0\Omega>0. For x∈Rnx\in\mathbb{R}^n put

βi(x)=Ω∑j∈Jiaij2xj2,bi+=bi+δmax⁡[1,∣bi∣].\beta_i(x) = \Omega\sqrt{\sum_{j\in J_i}a_{ij}^2x_j^2},\qquad b_i^+ = b_i+\delta\max[1,|b_i|].

If xx is feasible for the nominal problem (LP) and

∑jaijxj+ϵ βi(x)≤bi+∀i,\sum_j a_{ij}x_j + \epsilon\,\beta_i(x) \le b_i^+ \qquad \forall i,

then there exist y=(yij)y=(y_{ij}) and z=(zij)z=(z_{ij}) such that (x,y,z)(x,y,z) is feasible for (RC[ε, δ, Ω]).

Compared with the necessary and sufficient condition ∑jaijxj+ϵαi(x)≤bi+\sum_j a_{ij}x_j+\epsilon\alpha_i(x)\le b_i^+ for (IRC), with αi(x)=∑j∈Ji∣aij∣∣xj∣\alpha_i(x)=\sum_{j\in J_i}|a_{ij}||x_j|, this shows how much less restrictive (RC) can be when the sets JiJ_i are large.

Preamble
import Mathlib
import Definitions.Def_RobustLP_Counterpart_UncertainLP
import Definitions.Def_RobustLP_Counterpart_RobustCounterparts
Formal statement
namespace RobustLP.Counterpart

/-- **Sufficient condition for extending `x` to (RC)** (Ben-Tal–Nemirovski 2000, §3.1, p. 420).
For `ε > 0`, `δ > 0`, `Ω > 0`: if `x` is feasible for (LP) and
`∑_j a_{ij} x_j + ε β_i(x) ≤ b_i + δ max[1, |b_i|]` for every `i`, where
`β_i(x) = Ω √(∑_{j ∈ J_i} a_{ij}² x_j²)`, then `x` extends to a feasible solution `(x, y, z)` of
(RC[ε, δ, Ω]). -/
theorem rc_extension_of_beta {n p m : ℕ} (L : UncertainLP n p m)
    (ε δ Ω : ℝ) (hε : 0 < ε) (hδ : 0 < δ) (hΩ : 0 < Ω) (x : Fin n → ℝ)
    (hLP : L.NominalFeasible x)
    (hβ : ∀ i : Fin m, ∑ j, L.A i j * x j +
      ε * (Ω * Real.sqrt (∑ j ∈ L.J i, L.A i j ^ 2 * x j ^ 2)) ≤ L.bPlus δ i) :
    ∃ y z : Fin m → Fin n → ℝ, L.RCFeasible ε δ Ω x y z := by sorry

end RobustLP.Counterpart
Source
Ben-Tal and Nemirovski, Robust solutions of Linear Programming problems contaminated with uncertain data, Math. Program. Ser. A 88 (2000) 411–424, p. 420, §3.1, 'while a sufficient condition for x to admit an extension to a feasible solution of (RC) is …'
Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Sep 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph