Prove2Me

Theorem 2 — the tight set {j:v^j=rj}\{j : \hat v_j = r_j\} of an optimal dual solution is an optimal assortment

Proved
MarkovChainChoice.SingleResource.dual_tight_set_optimal

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

assortment-optimizationchoice-modelsdualitylinear-programmingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let (λ,ρ)(\lambda,\rho) be a Markov chain choice model with the standing assumptions and let r∈Rnr\in\mathbb R^n be arbitrary product revenues. Let v^\hat v be an optimal solution of the (Dual) linear program

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

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.

The theorem reduces assortment optimization under the Markov chain choice model to a linear program. In the single-resource problem it is applied in each period with the adjusted revenues rj−ΔVt+1(x)r_j-\Delta V_{t+1}(x), which may be negative.

Formalization Note The statement holds for every optimal v^\hat v (the paper speaks of "the" optimal solution; no uniqueness is assumed). No sign condition is placed on rr. This is the goal theorem of the companion mission I of this series, restated here because draft items cannot import one another.

Preamble
import Mathlib
import Definitions.Def_MarkovChainChoice_SingleResource_Assortment
open MarkovChainChoice.Shared
Formal statement
namespace MarkovChainChoice.SingleResource

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.SingleResource
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