Prove2Me

Lemma 11 (as quoted on p. 1332) — z^j≥Rj,Sx^\hat z_j\ge R_{j,S_{\hat x}} on H\mathcal H

Proved
MarkovChainChoice.DimReduction.visitNot_le_of_mem_H

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

z^j ≥ Rj,Sx^for all j∈N.\hat z_j\ \ge\ R_{j,S_{\hat x}}\qquad\text{for all } j\in N .

In words, z^\hat z dominates the visit-count vector of the (Balance) solution for the offer set given by the support of x^\hat x.

This comparison is the input to the bound α≤1\alpha\le1 on the step size of the Dimension Reduction algorithm and to the nonnegativity of the updated zz in Lemma 8.

Formalization Note The paper proves this as Lemma 11 in its online appendix, which is not reproduced here; the statement is the one quoted in the main text on p. 1332.

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 visitNot_le_of_mem_H {n : ℕ} (M : Model n) :
    ∀ p ∈ H M, ∀ j, visitNot M (drSupp p.1) j ≤ p.2 j := 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, quoting Lemma 11 of Online Appendix E
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