Prove2Me

Proof of Proposition 4, the special case ρ≤e−2+e−1\rho \le e^{-2+e^{-1}} — the maximizer p1∗=e−1+e−1p_1^* = e^{-1+e^{-1}}, p2∗=p1∗/ep_2^* = p_1^*/e

Proved
SeasonalPricing.MyopicDet.reducedObjective_special_case

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

calculusdynamic-pricingp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1revenue-management

Let 0<ρ≤e−2+e−10 < \rho \le e^{-2+e^{-1}} and

G(p1,p2)=(p1−p2)⋅ln⁡p1ln⁡ρ+p2⋅ln⁡p2ln⁡ρ,ρ≤p2≤p1≤1.G(p_1, p_2) = (p_1 - p_2)\cdot\frac{\ln p_1}{\ln\rho} + p_2\cdot\frac{\ln p_2}{\ln\rho}, \qquad \rho \le p_2 \le p_1 \le 1 .

Write p1∗=e−1+e−1p_1^* = e^{-1+e^{-1}} and p2∗=p1∗/e=e−2+e−1p_2^* = p_1^*/e = e^{-2+e^{-1}}. Then:

  1. the maximum of GG over the region ρ≤p2≤p1≤1\rho \le p_2 \le p_1 \le 1 exists and equals −e−1+e−1/ln⁡ρ-e^{-1+e^{-1}}/\ln\rho;
  2. (p1∗,p2∗)(p_1^*, p_2^*) lies in the region (ρ≤p2∗\rho \le p_2^* and p1∗≤1p_1^* \le 1) and G(p1∗,p2∗)=−e−1+e−1/ln⁡ρG(p_1^*, p_2^*) = -e^{-1+e^{-1}}/\ln\rho;
  3. (p1∗,p2∗)(p_1^*, p_2^*) is the only maximizer in the region.

The paper states "the special case ρ≤e−2+e−1\rho \le e^{-2+e^{-1}} could be easily solved analytically to yield the results stated in the proposition"; this item is that calculation. Uniqueness is stated because Proposition 4 names "the prices p1∗p_1^* and p2∗p_2^* that solve the problem" and gives their values.

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

/-- Proof of Proposition 4, the special case (Aviv–Pazgal 2008, pp. 351, 359): if
`0 < ρ ≤ e^{−2+e^{−1}}`, the maximum of `(p₁ − p₂) ln(p₁)/ln(ρ) + p₂ ln(p₂)/ln(ρ)` over
`ρ ≤ p₂ ≤ p₁ ≤ 1` equals `−e^{−1+e^{−1}}/ln(ρ)`, and it is attained exactly at
`p₁* = e^{−1+e^{−1}}`, `p₂* = p₁*/e`. -/
theorem reducedObjective_special_case (ρ : ℝ) (hρ0 : 0 < ρ)
    (hρ : ρ ≤ Real.exp (-2 + Real.exp (-1))) :
    IsGreatest {g : ℝ | ∃ p1 p2 : ℝ, ρ ≤ p2 ∧ p2 ≤ p1 ∧ p1 ≤ 1 ∧ g = reducedObjective ρ p1 p2}
        (-Real.exp (-1 + Real.exp (-1)) / Real.log ρ) ∧
      ρ ≤ Real.exp (-1 + Real.exp (-1)) / Real.exp 1 ∧
      Real.exp (-1 + Real.exp (-1)) ≤ 1 ∧
      reducedObjective ρ (Real.exp (-1 + Real.exp (-1)))
          (Real.exp (-1 + Real.exp (-1)) / Real.exp 1) =
        -Real.exp (-1 + Real.exp (-1)) / Real.log ρ ∧
      ∀ p1 p2 : ℝ, ρ ≤ p2 → p2 ≤ p1 → p1 ≤ 1 →
        reducedObjective ρ p1 p2 = -Real.exp (-1 + Real.exp (-1)) / Real.log ρ →
          p1 = Real.exp (-1 + Real.exp (-1)) ∧ p2 = Real.exp (-1 + Real.exp (-1)) / Real.exp 1 := 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. 351, Proposition 4 (p*₁ = e^{−1+e^{−1}}, p*₂ = p*₁/e); p. 359, Proof of Proposition 4 ("The special case …")
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