Prove2Me

(Dual) has an optimal solution and its value equals that of the linear program over H\mathcal H

Proved
MarkovChainChoice.Assortment.dual_value_eq_lp_value

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

choice-modelslp-dualityp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let (λ,ρ)(\lambda,\rho) be a Markov chain choice model on N={1,…,n}N=\{1,\dots,n\} and r∈Rnr\in\mathbb R^n revenues. The problem

min⁡v∈Rn{∑j∈Nλjvj: vj≥rj  ∀j∈N,  vj≥∑i∈Nρj,ivi  ∀j∈N}(Dual)\min_{v\in\mathbb R^n}\Big\{\sum_{j\in N}\lambda_jv_j:\ v_j\ge r_j\ \ \forall j\in N,\ \ v_j\ge\sum_{i\in N}\rho_{j,i}v_i\ \ \forall j\in N\Big\}\qquad\text{(Dual)}

has an optimal solution, and for every optimal solution v^\hat v of (Dual) and every optimal solution (x⋆,z⋆)(x^\star,z^\star) of the linear program max⁡{∑jrjxj:(x,z)∈H}\max\{\sum_j r_jx_j:(x,z)\in\mathcal H\},

∑j∈Nλjv^j=∑j∈Nrjxj⋆.\sum_{j\in N}\lambda_j\hat v_j=\sum_{j\in N}r_jx^\star_j .

(Dual) is the linear programming dual of the program over H\mathcal H; this is strong duality for that pair.

Formalization Note. Optimality on both sides is "feasible and at least as good as every feasible point".

Preamble
import Mathlib
import Definitions.Def_MarkovChainChoice_Assortment_Model
import Definitions.Def_MarkovChainChoice_Assortment_LinearPrograms
Formal statement
namespace MarkovChainChoice.Assortment

theorem dual_value_eq_lp_value {n : ℕ} (M : Model n) (r : Fin n → ℝ) :
    (∃ v, IsDualOptimal M r v) ∧
    ∀ (v : Fin n → ℝ) (p : (Fin n → ℝ) × (Fin n → ℝ)),
      IsDualOptimal M r v → IsLPOptimal M r p → ∑ j, M.lam j * v j = lpObjective r p := by sorry

end MarkovChainChoice.Assortment
Source
Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1326, Section 3, display (Dual)
Human review

  • Endorsed by Shuze Chen · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

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

View graph