Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Marginal values of capacity decrease in capacity and increase with the time remaining

Proved
MarkovChainChoice.SingleResource.marginal_value_monotone

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

concavitydynamic-programmingp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1revenue-management

Let (λ,ρ)(\lambda,\rho)(λ,ρ) be a Markov chain choice model with the standing assumptions and ∑j∈Nλj≤1\sum_{j\in N}\lambda_j\le 1∑j∈N​λj​≤1, let r∈Rnr\in\mathbb R^nr∈Rn be the product revenues and TTT the number of periods. Write ΔVt(x)=Vt(x)−Vt(x−1)\Delta V_t(x)=V_t(x)-V_t(x-1)ΔVt​(x)=Vt​(x)−Vt​(x−1) for the value functions of the (Single Resource) dynamic program. Then

ΔVt(x)≤ΔVt(x−1)for 1≤t≤T+1, x≥2,\Delta V_{t}(x)\le\Delta V_{t}(x-1)\qquad\text{for } 1\le t\le T+1,\ x\ge2,ΔVt​(x)≤ΔVt​(x−1)for 1≤t≤T+1, x≥2, ΔVt+1(x)≤ΔVt(x)for 1≤t≤T, x≥1.\Delta V_{t+1}(x)\le\Delta V_{t}(x)\qquad\text{for } 1\le t\le T,\ x\ge1.ΔVt+1​(x)≤ΔVt​(x)for 1≤t≤T, x≥1.

That is, the marginal value of capacity increases as fewer units remain and as more periods remain.

The paper attributes this to Talluri and van Ryzin (2004), for any choice model, and uses both inequalities in the proof of Theorem 5. The same result for an abstract choice model is published on Prove2Me as RevenueManagement.choice_marginal_values; taking its arrival probabilities equal to 111 and its choice model equal to Pj,SP_{j,S}Pj,S​ gives this statement.

Formalization Note The paper states the inequalities for ΔVt+1\Delta V_{t+1}ΔVt+1​; the index ranges above are the ones the proof of Theorem 5 uses (t=T+1t=T+1t=T+1 is trivial since VT+1=0V_{T+1}=0VT+1​=0). One hypothesis is added and disclosed: ∑jλj≤1\sum_j\lambda_j\le 1∑j​λj​≤1, which the paper's description (at most one customer per period, arriving to purchase jjj with probability λj\lambda_jλj​) implies and which makes 1−∑jPj,S1-\sum_jP_{j,S}1−∑j​Pj,S​ a probability. No sign condition is placed on the revenues rjr_jrj​, as on the page (the published Talluri–van Ryzin statement assumes nonnegative prices; this statement does not need them). Capacities are not bounded by ccc; the statement for every xxx contains the one for x≤cx\le cx≤c.

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

theorem marginal_value_monotone {n : ℕ} (M : Model n) (r : Fin n → ℝ) (T : ℕ)
    (hlam : ∑ j, M.lam j ≤ 1) :
    (∀ t x, 1 ≤ t → t ≤ T + 1 → 2 ≤ x →
        deltaValue M r T t x ≤ deltaValue M r T t (x - 1)) ∧
      ∀ t x, 1 ≤ t → t ≤ T → 1 ≤ x →
        deltaValue M r T (t + 1) x ≤ deltaValue M r T t x := by sorry

end MarkovChainChoice.SingleResource
Source
Feldman, Topaloglu, Revenue Management Under the Markov Chain Choice Model, Oper. Res. 65(5), 2017, p. 1329, proof of Theorem 5, second sentence (citing Talluri and van Ryzin 2004)
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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me