Prove2Me

The optimal value of (Assortment) equals the optimal value of the linear program over H\mathcal H

Proved
MarkovChainChoice.Assortment.assortment_value_eq_lp_value

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

assortment-optimizationchoice-modelslinear-programmingp2o-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 linear program

max⁡(x,z)∈R+2n{∑j∈Nrjxj: xj+zj=λj+∑i∈Nρi,jzi  ∀j∈N}\max_{(x,z)\in\mathbb R^{2n}_+}\Big\{\sum_{j\in N}r_jx_j:\ x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \ \forall j\in N\Big\}

has an optimal solution, and for every optimal solution (x⋆,z⋆)(x^\star,z^\star) of it and every optimal solution S⋆S^\star of the assortment problem max⁡S⊆N∑j∈NPj,Srj\max_{S\subseteq N}\sum_{j\in N}P_{j,S}r_j,

∑j∈NPj,S⋆rj=∑j∈Nrjxj⋆.\sum_{j\in N}P_{j,S^\star}r_j=\sum_{j\in N}r_jx^\star_j .

So the optimal expected revenue over all 2n2^n offer sets is obtained by solving one linear program.

Formalization Note. Both optima are stated with attainment: the linear program's optimum is asserted to exist, and an optimal assortment always exists because there are finitely many offer sets.

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

theorem assortment_value_eq_lp_value {n : ℕ} (M : Model n) (r : Fin n → ℝ) :
    (∃ p, IsLPOptimal M r p) ∧
    ∀ (S : Finset (Fin n)) (p : (Fin n → ℝ) × (Fin n → ℝ)),
      IsOptimalAssortment M r S → IsLPOptimal M r p → revenue M r S = 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 following Lemma 1
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