Prove2Me

Lemma 1 — an extreme point (x̂, ẑ) of ℋ equals (P_S, R_S) for S = {j : x̂_j > 0}

Proved
MarkovChainChoice.Reduced.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 (x^,z^)(\hat x,\hat z) be an extreme point of the polyhedron

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

and let Sx^={j∈N:x^j>0}S_{\hat x} = \{j\in N : \hat x_j > 0\} be the support of x^\hat x. 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 extreme point of H\mathcal H is therefore the purchase/non-purchase visit vector of some offer set, which links the geometry of H\mathcal H to assortments.

Formalization Note Extreme points are Mathlib's Set.extremePoints ℝ (H M) in the product space (Fin n → ℝ) × (Fin n → ℝ); the support is Finset.univ.filter (fun i => 0 < x i).

Preamble
import Mathlib
import Definitions.Def_MarkovChainChoice_Reduced_Model
import Definitions.Def_MarkovChainChoice_Reduced_LinearPrograms
Formal statement
namespace MarkovChainChoice.Reduced

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