Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 2 — the constant rate λ^D = min{λ*, x/t} solves the deterministic problem (11); J^D(x,t) = t r(λ^D)

Proved
GVRPricing.FixedPrice.deterministic_solution

by mikedeng1 · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

deterministic-controlfluid-approximationp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1revenue-management

Let (Λ,p,λ∗)(\Lambda,p,\lambda^*)(Λ,p,λ∗) be a regular demand function, x≥0x\ge0x≥0 a stock and t>0t>0t>0 a horizon. Write λ0=x/t\lambda^0=x/tλ0=x/t for the run-out rate, p0=p(λ0)p^0=p(\lambda^0)p0=p(λ0) and r0=p0λ0r^0=p^0\lambda^0r0=p0λ0, and set

λD=min⁡{λ∗,λ0}.\lambda^D=\min\{\lambda^*,\lambda^0\}.λD=min{λ∗,λ0}.

Then:

  1. the constant path λ(s)=λD\lambda(s)=\lambda^Dλ(s)=λD, 0≤s≤t0\le s\le t0≤s≤t, is feasible for the deterministic problem (11);
  2. it is optimal: every feasible rate path λ(⋅)\lambda(\cdot)λ(⋅) satisfies ∫0tr(λ(s)) ds≤t r(λD)\int_0^t r(\lambda(s))\,ds\le t\,r(\lambda^D)∫0t​r(λ(s))ds≤tr(λD);
  3. the optimal revenue is
JD(x,t)=t r(λD),J^D(x,t)=t\,r(\lambda^D),JD(x,t)=tr(λD),

which equals tmin⁡{r∗,r0}t\min\{r^*,r^0\}tmin{r∗,r0} when x≤λ∗tx\le\lambda^*tx≤λ∗t, and t r∗t\,r^*tr∗ when x≥λ∗tx\ge\lambda^*tx≥λ∗t; 4. in terms of price, pD=p(λD)=max⁡{p∗,p0}p^D=p(\lambda^D)=\max\{p^*,p^0\}pD=p(λD)=max{p∗,p0} (when λ∗>0\lambda^*>0λ∗>0, x>0x>0x>0 and λ0∈Λ\lambda^0\in\Lambdaλ0∈Λ, so that both prices are finite).

If items are plentiful (x≥λ∗tx\ge\lambda^*tx≥λ∗t) the firm prices at the revenue-maximizing level; if they are scarce it prices to sell exactly its stock. This solution supplies the fixed-price heuristic and the value against which Theorems 2 and 3 compare the stochastic problem.

Formalization Note The page prints JD(x,t)=tmin⁡{r∗,r0}J^D(x,t)=t\min\{r^*,r^0\}JD(x,t)=tmin{r∗,r0} (eq. (12)) without a case distinction. That is wrong when x>λ∗tx>\lambda^*tx>λ∗t: there r0=r(λ0)≤r∗r^0=r(\lambda^0)\le r^*r0=r(λ0)≤r∗, so tmin⁡{r∗,r0}=t r0t\min\{r^*,r^0\}=t\,r^0tmin{r∗,r0}=tr0, while the optimum is t r∗t\,r^*tr∗. For exponential demand ae−pae^{-p}ae−p with x=atx=atx=at, r0=0r^0=0r0=0 but JD=at/eJ^D=a t/eJD=at/e. The statement gives the corrected value t r(λD)t\,r(\lambda^D)tr(λD), and the printed form in the case x≤λ∗tx\le\lambda^*tx≤λ∗t, where it is right. The page calls λD\lambda^DλD "the" optimal solution; under concavity alone it need not be unique, so the statement asserts optimality, not uniqueness. When λ0∉Λ\lambda^0\notin\Lambdaλ0∈/Λ the run-out quantities p0p^0p0, r0r^0r0 are undefined, and the statement uses them only where λ0∈Λ\lambda^0\in\Lambdaλ0∈Λ. The OCR's "p(λ0)p(\lambda_0)p(λ0​)" is a typesetting slip for p(λ0)p(\lambda^0)p(λ0).

Preamble
import Mathlib
import Definitions.Def_GVRPricing_FixedPrice_Model
import Definitions.Def_GVRPricing_FixedPrice_Deterministic

open MeasureTheory Set
Formal statement
namespace GVRPricing.FixedPrice

/-- **Proposition 2** (p. 1006), with the value (12) corrected. For a stock `x ≥ 0` and a
horizon `t > 0`, with run-out rate `λ⁰ = x/t` and `λ^D = min{λ*, λ⁰}`:
1. the constant path `λ(s) = λ^D` is feasible for (11);
2. it is optimal: every feasible rate path earns at most `∫_0^t r(λ^D) ds`;
3. the optimal revenue is `J^D(x, t) = t r(λ^D)`, which equals `t min{r*, r⁰}` (`r⁰ = r(λ⁰)`)
   when `x ≤ λ* t` and `t r*` when `x ≥ λ* t` (the printed `t min{r*, r⁰}` is wrong for
   `x > λ* t`, where `r⁰ ≤ r*`);
4. in terms of price, `p^D = p(λ^D) = max{p*, p⁰}` whenever both prices are finite
   (`λ* > 0`, `x > 0`, `λ⁰ ∈ Λ`). -/
theorem deterministic_solution (M : Model) (x t : ℝ) (hx : 0 ≤ x) (ht : 0 < t) :
    IsFeasiblePath M x t (fun _ => min M.lstar (x / t)) ∧
    (∀ ℓ : ℝ → ℝ, IsFeasiblePath M x t ℓ →
      ∫ s in (0 : ℝ)..t, M.r (ℓ s) ≤ ∫ s in (0 : ℝ)..t, M.r (min M.lstar (x / t))) ∧
    detValue M x t = t * M.r (min M.lstar (x / t)) ∧
    (x ≤ M.lstar * t → detValue M x t = t * min M.rstar (M.r (x / t))) ∧
    (M.lstar * t ≤ x → detValue M x t = t * M.rstar) ∧
    (0 < M.lstar → 0 < x → x / t ∈ M.Λ →
      M.p (min M.lstar (x / t)) = max M.pstar (M.p (x / t))) := by sorry

end GVRPricing.FixedPrice
Source
Gallego, van Ryzin, Optimal Dynamic Pricing of Inventories with Stochastic Demand over Finite Horizons, Management Science 40(8) (1994), p. 1006 (PDF 8), §3.2, Proposition 2, eq. (12)
Human review
  • Endorsed by Shuze Chen · Oct 5, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 5, 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