Prove2Me

Lemma 1 — extreme points of H\mathcal H are the (Balance) solutions (PS,RS)(P_S,R_S)

Proved
MarkovChainChoice.Assortment.extreme_point_eq_balance

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

choice-modelsextreme-pointsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1polyhedra

Let (λ,ρ)(\lambda,\rho) be a Markov chain choice model and H={(x,z)∈R+2n:xj+zj=λj+∑i∈Nρi,jzi ∀j}\mathcal H=\{(x,z)\in\mathbb R^{2n}_+: x_j+z_j=\lambda_j+\sum_{i\in N}\rho_{i,j}z_i\ \forall j\}. For an extreme point (x^,z^)(\hat x,\hat z) of H\mathcal H, let Sx^={j∈N:x^j>0}S_{\hat x}=\{j\in N:\hat x_j>0\}. Then

Pj,Sx^=x^jandRj,Sx^=z^jfor all j∈N.P_{j,S_{\hat x}}=\hat x_j\quad\text{and}\quad R_{j,S_{\hat x}}=\hat z_j\qquad\text{for all } j\in N .

Every vertex of H\mathcal H is therefore the purchase/non-purchase visit vector of some offer set, which is the bridge from the combinatorial assortment problem to linear programming.

Formalization Note. Extreme points are Mathlib's Set.extremePoints ℝ (H M) in (Fin n → ℝ) × (Fin n → ℝ).

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

theorem extreme_point_eq_balance {n : ℕ} (M : Model n) (x z : Fin n → ℝ)
    (hext : (x, z) ∈ Set.extremePoints ℝ (H M)) :
    ∀ j, purchase M (Finset.univ.filter (fun i => 0 < x i)) j = x j ∧
      visitNot M (Finset.univ.filter (fun i => 0 < x i)) j = z j := by sorry

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