Section 7 — the step size $\alpha_{\hat x}$ is at most one on $\mathcal H$

Proved

MarkovChainChoice.DimReduction.drAlpha_le_one

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

choice-modelsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1polyhedra

Let $(\lambda,\rho)$ be a Markov chain choice model satisfying the standing assumptions, let $(\hat x,\hat z)\in\mathcal H$ , and suppose $S_{\hat x}=\{j\in N:\hat x_j>0\}$ is nonempty. Then

\alpha_{\hat x}=\min\Big\{\frac{\hat x_j}{P_{j,S_{\hat x}}}: j\in S_{\hat x}\Big\}\ \le\ 1 .

Hence Step 2 of the Dimension Reduction algorithm either stops ( $\alpha=1$ ) or produces $\alpha<1$ , so Step 3 is well defined.

Preamble

import Mathlib
import Definitions.Def_MarkovChainChoice_Shared_Model
import Definitions.Def_MarkovChainChoice_Shared_Balance
import Definitions.Def_MarkovChainChoice_DimReduction_H
import Definitions.Def_MarkovChainChoice_DimReduction_Algorithm
open MarkovChainChoice.Shared

Formal statement

namespace MarkovChainChoice.DimReduction

theorem drAlpha_le_one {n : ℕ} (M : Model n) :
    ∀ p ∈ H M, (drSupp p.1).Nonempty → drAlpha M p.1 ≤ 1 := by sorry

end MarkovChainChoice.DimReduction

Source

Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1332, Section 7, right column

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

Section 7 — the step size αx^\alpha_{\hat x}αx^​ is at most one on H\mathcal HH

Section 7 — the step size $\alpha_{\hat x}$ is at most one on $\mathcal H$