Proof of Theorem 7, p. 1331 — every point of ℋ is a positive convex combination of finitely many extreme points

Proved

MarkovChainChoice.Reduced.H_convex_comb_extreme_points

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

convexityextreme-pointsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1polyhedra

Let $(\hat x,\hat z)\in\mathcal H$ , where $\mathcal H$ is the polyhedron of the Markov chain choice model. Then there exist $K\ge 1$ , extreme points $(x^1,z^1),\dots,(x^K,z^K)$ of $\mathcal H$ , and positive scalars $\gamma^1,\dots,\gamma^K$ with $\sum_{k=1}^K\gamma^k = 1$ such that

\hat x = \sum_{k=1}^K\gamma^k x^k \qquad\text{and}\qquad \hat z = \sum_{k=1}^K \gamma^k z^k.

This is the representation of a point of the polytope $\mathcal H$ through its vertices; combined with Lemma 1 it expresses any point of $\mathcal H$ through the vectors $(P_S,R_S)$ .

Formalization Note $K$ is a natural number and the extreme points and weights are indexed by Fin K; the condition $\sum_k\gamma^k = 1$ forces $K\ge 1$ .

Preamble

import Mathlib
import Definitions.Def_MarkovChainChoice_Reduced_Model
import Definitions.Def_MarkovChainChoice_Reduced_LinearPrograms

Formal statement

namespace MarkovChainChoice.Reduced

theorem H_convex_comb_extreme_points {n : ℕ} (M : Model n) (x z : Fin n → ℝ)
    (hxz : (x, z) ∈ H M) :
    ∃ (K : ℕ) (p : Fin K → (Fin n → ℝ) × (Fin n → ℝ)) (γ : Fin K → ℝ),
      (∀ k, p k ∈ Set.extremePoints ℝ (H M)) ∧ (∀ k, 0 < γ k) ∧ ∑ k, γ k = 1 ∧
      x = ∑ k, γ k • (p k).1 ∧ z = ∑ k, γ k • (p k).2 := by sorry

end MarkovChainChoice.Reduced

Source

Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1331, proof of Theorem 7, 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