Prove2Me

Lemma 3 — lowering all revenues by η≥0\eta\ge0 shrinks the dual tight set

Proved
MarkovChainChoice.SingleResource.dual_tight_set_shrinks

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

assortment-optimizationchoice-modelslinear-programmingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let (λ,ρ)(\lambda,\rho) be a Markov chain choice model with the standing assumptions, r∈Rnr\in\mathbb R^n arbitrary revenues and η≥0\eta\ge 0. Let v^0\hat v^0 be an optimal solution of (Dual) with revenues rr, and let v^η\hat v^\eta be an optimal solution of (Dual) when the revenue of every product is decreased by η\eta, i.e. with revenues rj−ηr_j-\eta. Then

{j∈N: v^jη=rj−η} ⊆ {j∈N: v^j0=rj}.\{j\in N:\ \hat v^\eta_j=r_j-\eta\}\ \subseteq\ \{j\in N:\ \hat v^0_j=r_j\}.

Combined with Theorem 2, this says that decreasing all revenues by the same nonnegative amount makes the optimal assortment produced by the dual smaller. This is the step that turns monotonicity of marginal values into nested offer sets in Theorem 5.

Formalization Note The paper writes ⊂\subset for (non-strict) inclusion; it is rendered as ⊆\subseteq. Both dual solutions are arbitrary optimal solutions. No sign condition is placed on rr.

Preamble
import Mathlib
import Definitions.Def_MarkovChainChoice_SingleResource_Assortment
open MarkovChainChoice.Shared
Formal statement
namespace MarkovChainChoice.SingleResource

theorem dual_tight_set_shrinks {n : ℕ} (M : Model n) (r : Fin n → ℝ) (η : ℝ) (hη : 0 ≤ η)
    (v0 vη : Fin n → ℝ) (hv0 : IsDualOptimal M r v0)
    (hvη : IsDualOptimal M (fun j => r j - η) vη) :
    Finset.univ.filter (fun j => vη j = r j - η) ⊆
      Finset.univ.filter (fun j => v0 j = r j) := by sorry

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