Section 2 — the (Balance) equations have a unique and nonnegative solution

Proved

MarkovChainChoice.DimReduction.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 $\lambda_j>0$ , $\rho_{j,i}\ge0$ and $\sum_{i\in N}\rho_{j,i}<1$ for all $j,i\in N$ , and let $S\subseteq N$ be any offer set. Then the (Balance) equations

P_{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_S,R_S)$ , and this solution is nonnegative: $P_{j,S}\ge0$ and $R_{j,S}\ge0$ for all $j\in N$ .

This guarantees that the purchase probabilities $P_S$ and visit counts $R_S$ used by every other statement of the mission are well defined.

Formalization Note The conclusion is stated for the chosen solution (purchase M S, visitNot M S): it solves (Balance), it is nonnegative, and every solution of (Balance) equals it.

Preamble

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

Formal statement

namespace MarkovChainChoice.DimReduction

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

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