Prove2Me

Eq. (19) — case λ*t ≤ n: J^FP(n,t) ≥ p*(λ*t − (√(λ*t + (n − λ*t)²) − (n − λ*t))/2) ≥ r*t(1 − 1/(2√(λ*t)))

Proved
GVRPricing.FixedPrice.fp_abundant_bound

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

fixed-pricep2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1performance-guaranteerevenue-management

Let (Λ,p,λ∗)(\Lambda,p,\lambda^*) be a regular demand function with λ∗>0\lambda^*>0, nn a stock and t>0t>0 a horizon with λ∗t≤n\lambda^*t\le n, the case in which items are plentiful. The fixed-price heuristic then prices at p∗=p(λ∗)p^*=p(\lambda^*), and

JFP(n,t) ≥ p∗(λ∗t−λ∗t+(n−λ∗t)2−(n−λ∗t)2) ≥ p∗λ∗t(1−12λ∗t)=r∗t(1−12λ∗t).(19)J^{FP}(n,t)\ \ge\ p^*\Big(\lambda^*t-\frac{\sqrt{\lambda^*t+(n-\lambda^*t)^2}-(n-\lambda^*t)}{2}\Big)\ \ge\ p^*\lambda^*t\Big(1-\frac{1}{2\sqrt{\lambda^*t}}\Big)=r^*t\Big(1-\frac{1}{2\sqrt{\lambda^*t}}\Big).\qquad(19)

This is the second case of Theorem 3. Compared with JD(n,t)=r∗tJ^D(n,t)=r^*t (Proposition 2), it gives the ratio 1−1/(2λ∗t)1-1/(2\sqrt{\lambda^*t}).

Formalization Note The first inequality is stated for the embedding of a real number into [0,∞][0,\infty]; the other two are inequalities of real numbers. The hypothesis λ∗>0\lambda^*>0 makes 1/(2λ∗t)1/(2\sqrt{\lambda^*t}) defined; it is also a hypothesis of the goal theorem.

Preamble
import Mathlib
import Definitions.Def_GVRPricing_FixedPrice_Model
import Definitions.Def_GVRPricing_FixedPrice_SalesProcess

open MeasureTheory ProbabilityTheory Set
open scoped ENNReal
Formal statement
namespace GVRPricing.FixedPrice

/-- **Proof of Theorem 3, abundant case, eq. (19)** (p. 1008). If `λ* t ≤ n` (`t > 0`, `λ* > 0`),
the fixed-price heuristic uses `p* = p(λ*)` and
`J^FP(n, t) ≥ p*(λ*t − (√(λ*t + (n − λ*t)²) − (n − λ*t))/2) ≥ p*λ*t(1 − 1/(2√(λ*t)))
= r* t (1 − 1/(2√(λ*t)))`. -/
theorem fp_abundant_bound (M : Model) (n : ℕ) (t : ℝ) (ht : 0 < t) (hl : 0 < M.lstar)
    (h : M.lstar * t ≤ n) :
    ENNReal.ofReal (M.pstar * (M.lstar * t -
        (Real.sqrt (M.lstar * t + ((n : ℝ) - M.lstar * t) ^ 2) - ((n : ℝ) - M.lstar * t)) / 2))
      ≤ fpValue M n t ∧
    M.pstar * M.lstar * t * (1 - 1 / (2 * Real.sqrt (M.lstar * t))) ≤
      M.pstar * (M.lstar * t -
        (Real.sqrt (M.lstar * t + ((n : ℝ) - M.lstar * t) ^ 2) - ((n : ℝ) - M.lstar * t)) / 2) ∧
    M.pstar * M.lstar * t * (1 - 1 / (2 * Real.sqrt (M.lstar * t))) =
      M.rstar * t * (1 - 1 / (2 * Real.sqrt (M.lstar * 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. 1008 (PDF 10), §3.3, Proof of Theorem 3, eq. (19)
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