Prove2Me

The (Balance) equations have a unique, nonnegative solution (PS,RS)(P_S,R_S)

Proved
MarkovChainChoice.Assortment.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 on N={1,…,n}N=\{1,\dots,n\} 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 jj. 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 (PS,RS)(P_S,R_S), and it satisfies Pj,S≥0P_{j,S}\ge 0 and Rj,S≥0R_{j,S}\ge 0 for all j∈Nj\in N.

This is what makes the purchase probabilities Pj,SP_{j,S} well defined, and every later result is stated in terms of them.

Formalization Note. The statement is about the objects purchase M S and visitNot M S of the definition layer: they satisfy (Balance), are nonnegative, and coincide with every solution of (Balance).

Preamble
import Mathlib
import Definitions.Def_MarkovChainChoice_Assortment_Model
Formal statement
namespace MarkovChainChoice.Assortment

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