Prove2Me

Section 2, p. 1325 — (Balance) has a unique and nonnegative solution for every offer set

Proved
MarkovChainChoice.Reduced.balance_unique_nonneg

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 with λj>0\lambda_j>0, ρj,i≥0\rho_{j,i}\ge 0 and ∑i∈Nρj,i<1\sum_{i\in N}\rho_{j,i}<1 for all j∈Nj\in N. Then for every offer set S⊆NS\subseteq N the (Balance) equations

Pj+Rj=λj+∑i∈Nρi,jRi  ∀j∈N,Pj=0  ∀j∉S,Rj=0  ∀j∈SP_{j} + R_{j} = \lambda_j + \sum_{i\in N}\rho_{i,j}R_{i}\ \ \forall j\in N,\qquad P_{j} = 0\ \ \forall j\notin S,\qquad R_{j} = 0\ \ \forall j\in S

have exactly one solution (P,R)(P,R), and this solution is nonnegative. We denote it (PS,RS)(P_S,R_S).

This is what makes the purchase probabilities Pj,SP_{j,S} well defined; every later statement about (PS,RS)(P_S,R_S) relies on it.

Formalization Note The statement says that the chosen pair (purchase M S, visitNot M S) satisfies (Balance), is componentwise nonnegative, and equals every solution of (Balance).

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

theorem balance_unique_nonneg {n : ℕ} (M : Model n) (S : Finset (Fin n)) :
    IsBalance M S (purchase M S) (visitNot M S) ∧
    (∀ j, 0 ≤ purchase M S j) ∧ (∀ j, 0 ≤ visitNot M S j) ∧
    ∀ P R : Fin n → ℝ, IsBalance M S P R → P = purchase M S ∧ R = visitNot M S := by sorry

end MarkovChainChoice.Reduced
Source
Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1325, Section 2 (last sentence of the paragraph on (I − Q̄)^T R̄_S = λ̄)
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