Prove2Me

Theorem 2 — the products with v^j=rj\hat v_j=r_j form an optimal assortment

Proved
MarkovChainChoice.Assortment.dual_tight_set_optimal

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

assortment-optimizationchoice-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\} (with λj>0\lambda_j>0, ρj,i≥0\rho_{j,i}\ge0, ∑iρj,i<1\sum_i\rho_{j,i}<1) and r∈Rnr\in\mathbb R^n revenues. Let v^\hat v be an optimal solution of

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)}

and define S^={j∈N:v^j=rj}\hat S=\{j\in N:\hat v_j=r_j\}. Then S^\hat S is an optimal solution of the assortment problem:

∑j∈NPj,S rj ≤ ∑j∈NPj,S^ rjfor every S⊆N,\sum_{j\in N}P_{j,S}\,r_j\ \le\ \sum_{j\in N}P_{j,\hat S}\,r_j\qquad\text{for every } S\subseteq N,

where (PS,RS)(P_S,R_S) is the solution of the (Balance) equations for the offer set SS.

The assortment problem over 2n2^n offer sets is thereby solved by one linear program with nn variables, which makes it tractable.

Formalization Note. The theorem is stated for every optimal solution v^\hat v of (Dual) (the paper's "the optimal solution"; the proof uses only optimality). S^\hat S is defined by equality v^j=rj\hat v_j=r_j, and revenues carry no sign assumption.

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

theorem dual_tight_set_optimal {n : ℕ} (M : Model n) (r v : Fin n → ℝ)
    (hv : IsDualOptimal M r v) :
    IsOptimalAssortment M r (Finset.univ.filter (fun j => v j = r j)) := by sorry

end MarkovChainChoice.Assortment
Source
Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1326, Theorem 2
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