Section 2 — purchase probabilities are strictly positive on the offer set

Proved

MarkovChainChoice.DimReduction.purchase_pos

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

choice-modelsmarkov-chainsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $(\lambda,\rho)$ be a Markov chain choice model satisfying the standing assumptions ( $\lambda_j>0$ , $\rho_{j,i}\ge0$ , $\sum_i\rho_{j,i}<1$ ). For every offer set $S\subseteq N$ ,

P_{j,S}>0\qquad\text{for all } j\in S .

That is, each offered product is purchased with strictly positive probability.

In the Dimension Reduction algorithm this is what makes the ratios $x_j/P_{j,S}$ of Step 2 meaningful.

Preamble

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

Formal statement

namespace MarkovChainChoice.DimReduction

theorem purchase_pos {n : ℕ} (M : Model n) (S : Finset (Fin n)) :
    ∀ j ∈ S, 0 < purchase M S j := by sorry

end MarkovChainChoice.DimReduction

Source

Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1325, Section 2, left 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