Prove2Me

Proof of Proposition 4, third observation — on [τ1,τ2][\tau_1, \tau_2] the revenue is λG(p1,p2)\lambda G(p_1, p_2)

Proved
SeasonalPricing.MyopicDet.revenue_eq_reducedObjective

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

dynamic-pricingmarkdown-pricingp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1revenue-management

Let λ>0\lambda > 0 and 0<ρ<10 < \rho < 1, and consider myopic customers with identical base valuation 11, valuation ρt\rho^t at time tt, season [0,1][0, 1] and unlimited inventory, with expected revenue Rρ(p1,p2;T)R_\rho(p_1, p_2; T). Let ρ≤p2≤p1≤1\rho \le p_2 \le p_1 \le 1, τ1=ln⁡(p1)/ln⁡(ρ)\tau_1 = \ln(p_1)/\ln(\rho) and τ2=ln⁡(p2)/ln⁡(ρ)\tau_2 = \ln(p_2)/\ln(\rho). Then for every discount time T∈[τ1,τ2]T \in [\tau_1, \tau_2],

Rρ(p1,p2;T)=λ[(p1−p2)⋅ln⁡p1ln⁡ρ+p2⋅ln⁡p2ln⁡ρ].R_\rho(p_1, p_2; T) = \lambda\left[(p_1 - p_2)\cdot\frac{\ln p_1}{\ln\rho} + p_2\cdot\frac{\ln p_2}{\ln\rho}\right].

In particular the revenue does not depend on where in [τ1,τ2][\tau_1, \tau_2] the discount is offered. Together with the first two observations this reduces the seller's problem over prices and discount time to the maximization of the bracket over ρ≤p2≤p1≤1\rho \le p_2 \le p_1 \le 1.

Preamble
import Mathlib
import Definitions.Def_SeasonalPricing_MyopicDet_myopicRevenue
import Definitions.Def_SeasonalPricing_MyopicDet_reducedObjective
Formal statement
namespace SeasonalPricing.MyopicDet

/-- Proof of Proposition 4, third observation (Aviv–Pazgal 2008, p. 359): for prices
`ρ ≤ p₂ ≤ p₁ ≤ 1` and any discount time `T ∈ [τ₁, τ₂]`, the expected revenue equals
`λ · [(p₁ − p₂) · ln(p₁)/ln(ρ) + p₂ · ln(p₂)/ln(ρ)]`, independently of `T`. -/
theorem revenue_eq_reducedObjective (lam ρ p1 p2 T : ℝ) (hlam : 0 < lam) (hρ0 : 0 < ρ)
    (hρ1 : ρ < 1) (hp2 : ρ ≤ p2) (hp12 : p2 ≤ p1) (hp1 : p1 ≤ 1)
    (hT1 : tau ρ p1 ≤ T) (hT2 : T ≤ tau ρ p2) :
    detRevenue lam ρ p1 p2 T = lam * reducedObjective ρ p1 p2 := by sorry

end SeasonalPricing.MyopicDet
Source
Aviv and Pazgal, Optimal Pricing of Seasonal Products in the Presence of Forward-Looking Consumers, Manufacturing & Service Operations Management 10(3), 2008, p. 359, Proof of Proposition 4 ("Third, …")
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