Prove2Me

Lemma 8 — one step of Dimension Reduction stays in H\mathcal H and drops the minimizing product

Proved
MarkovChainChoice.DimReduction.lemma_8

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

choice-modelsconvex-decompositionp2o-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. Define Sx^={j∈N:x^j>0}S_{\hat x}=\{j\in N:\hat x_j>0\}, assume it is nonempty, and let

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

with jx^∈Sx^j_{\hat x}\in S_{\hat x} any index attaining this minimum. Assume αx^<1\alpha_{\hat x}<1 and define

u^j=x^j−αx^Pj,Sx^1−αx^,v^j=z^j−αx^Rj,Sx^1−αx^(j∈N),\hat u_j=\frac{\hat x_j-\alpha_{\hat x}P_{j,S_{\hat x}}}{1-\alpha_{\hat x}},\qquad \hat v_j=\frac{\hat z_j-\alpha_{\hat x}R_{j,S_{\hat x}}}{1-\alpha_{\hat x}}\qquad (j\in N),

and Su^={j∈N:u^j>0}S_{\hat u}=\{j\in N:\hat u_j>0\}. Then (u^,v^)∈H(\hat u,\hat v)\in\mathcal H and Su^⊆Sx^∖{jx^}S_{\hat u}\subseteq S_{\hat x}\setminus\{j_{\hat x}\}.

Since (x^,z^)=αx^(PSx^,RSx^)+(1−αx^)(u^,v^)(\hat x,\hat z)=\alpha_{\hat x}(P_{S_{\hat x}},R_{S_{\hat x}})+(1-\alpha_{\hat x})(\hat u,\hat v), the lemma is the single step of the Dimension Reduction algorithm: it peels off one (Balance) solution and leaves a point of H\mathcal H with strictly smaller support.

Formalization Note The paper's jx^=arg⁡min⁡j_{\hat x}=\arg\min may not be unique; the statement holds for every minimizer. The paper writes ⊂\subset for (not necessarily strict) inclusion; the conclusion uses ⊆\subseteq, and strictness is already carried by the removal of jx^j_{\hat x}.

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 lemma_8 {n : ℕ} (M : Model n) (p : (Fin n → ℝ) × (Fin n → ℝ)) (hp : p ∈ H M)
    (hS : (drSupp p.1).Nonempty) (hα : drAlpha M p.1 < 1)
    (jbar : Fin n) (hjbar : jbar ∈ drSupp p.1)
    (hmin : p.1 jbar / purchase M (drSupp p.1) jbar = drAlpha M p.1) :
    drNext M p ∈ H M ∧ drSupp (drNext M p).1 ⊆ (drSupp p.1).erase jbar := by sorry

end MarkovChainChoice.DimReduction
Source
Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1333, Lemma 8
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