Prove2Me

An optimal solution of (Dual) is tight in one of its two constraints at every product

Proved
MarkovChainChoice.Assortment.dual_optimal_tight

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\}, r∈Rnr\in\mathbb R^n revenues, and v^\hat v an optimal solution of

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

Then for each j∈Nj\in N,

v^j=rjorv^j=∑i∈Nρj,iv^i.\hat v_j=r_j\qquad\text{or}\qquad \hat v_j=\sum_{i\in N}\rho_{j,i}\hat v_i .

This complementary-slackness type property identifies, product by product, whether the dual solution is pinned by the revenue or by the continuation value.

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

theorem dual_optimal_tight {n : ℕ} (M : Model n) (r v : Fin n → ℝ)
    (hv : IsDualOptimal M r v) :
    ∀ j, v j = r j ∨ v j = ∑ i, M.rho j i * v i := by sorry

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