Prove2Me

Section 7, first case — a point of H\mathcal H with Sx^=∅S_{\hat x}=\emptyset equals (P∅,R∅)(P_\emptyset,R_\emptyset)

Proved
MarkovChainChoice.DimReduction.eq_balance_of_supp_empty

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

choice-modelsp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1polyhedra

Let (λ,ρ)(\lambda,\rho) be a Markov chain choice model satisfying the standing assumptions and let (x^,z^)∈H(\hat x,\hat z)\in\mathcal H. If Sx^={j∈N:x^j>0}=∅S_{\hat x}=\{j\in N:\hat x_j>0\}=\emptyset, then

(x^,z^)=(P∅,R∅),(\hat x,\hat z)=(P_\emptyset,R_\emptyset),

the solution of the (Balance) equations for the empty offer set.

This is the configuration in which the Dimension Reduction algorithm stops in Step 1.

Preamble
import Mathlib
import Definitions.Def_MarkovChainChoice_Shared_Model
import Definitions.Def_MarkovChainChoice_Shared_Balance
import Definitions.Def_MarkovChainChoice_DimReduction_H
import Definitions.Def_MarkovChainChoice_DimReduction_Algorithm
open MarkovChainChoice.Shared
Formal statement
namespace MarkovChainChoice.DimReduction

theorem eq_balance_of_supp_empty {n : ℕ} (M : Model n) :
    ∀ p ∈ H M, drSupp p.1 = ∅ → p = (purchase M ∅, visitNot M ∅) := by sorry

end MarkovChainChoice.DimReduction
Source
Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1332, Section 7, right column (first case)
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