Prove2Me

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

Proved
MarkovChainChoice.SingleResource.balance_unique_nonneg

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

choice-modelslinear-algebramarkov-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}\ge0 and ∑i∈Nρj,i<1\sum_{i\in N}\rho_{j,i}<1 for all j∈Nj\in N, and let S⊆NS\subseteq N be any offer set. Then 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. In particular the pair (PS,RS)(P_S,R_S) used throughout the paper is well defined, and Pj,S≥0P_{j,S}\ge 0, Rj,S≥0R_{j,S}\ge0.

This is what makes the purchase probabilities Pj,SP_{j,S} meaningful objects in the assortment problem and the dynamic program.

Formalization Note (PS,RS)(P_S,R_S) is the pair (purchase M S, visitNot M S) chosen by Classical.epsilon; the theorem states that it solves (Balance), that both vectors are nonnegative, and that every solution of (Balance) equals it.

Preamble
import Mathlib
import Definitions.Def_MarkovChainChoice_Shared_Balance
open MarkovChainChoice.Shared
Formal statement
namespace MarkovChainChoice.SingleResource

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.SingleResource
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