Prove2Me

Section 7, second case — a point of H\mathcal H with αx^=1\alpha_{\hat x}=1 equals (PSx^,RSx^)(P_{S_{\hat x}},R_{S_{\hat x}})

Proved
MarkovChainChoice.DimReduction.eq_balance_of_alpha_eq_one

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 with Sx^={j∈N:x^j>0}S_{\hat x}=\{j\in N:\hat x_j>0\} nonempty. If

αx^=min⁡{x^jPj,Sx^:j∈Sx^}=1,\alpha_{\hat x}=\min\Big\{\frac{\hat x_j}{P_{j,S_{\hat x}}}: j\in S_{\hat x}\Big\}=1,

then x^=PSx^\hat x=P_{S_{\hat x}} and z^=RSx^\hat z=R_{S_{\hat x}}.

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

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_alpha_eq_one {n : ℕ} (M : Model n) :
    ∀ p ∈ H M, (drSupp p.1).Nonempty → drAlpha M p.1 = 1 →
      p = (purchase M (drSupp p.1), visitNot M (drSupp p.1)) := 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 (second 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