Eq. (9) — $r_\alpha(d) = \alpha - (1 - \alpha) M_\alpha(d)$

Proved

VeinottWagnerSS.RenewalCost.eq9_rAlpha_closed_form

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

inventoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1renewal-theory

Let $\varphi$ be a demand distribution and $0 \le \alpha \le 1$ with $\alpha\varphi(0) < 1$ . For every $d = 0, 1, \dots$ , the expected discount factor of the first period in which cumulative demand exceeds $d$ ,

r_\alpha(d) = \sum_{i=1}^{\infty} \alpha^i\bigl[\Phi^{i-1}(d) - \Phi^i(d)\bigr],

equals

r_\alpha(d) = \alpha - (1 - \alpha) M_\alpha(d).

It expresses the discounted set-up factor through the discount renewal function; in particular $1 - r_\alpha(d) = (1-\alpha)(1 + M_\alpha(d))$ .

Formalization Note $r_\alpha$ is defined by the first line of (9), i.e. as $E[\alpha^{T(d)}]$ computed from the law $\Pr[T(d) = i] = \Phi^{i-1}(d) - \Phi^i(d)$ .

Preamble

import Mathlib
import Definitions.Def_VeinottWagnerSS_RenewalCost_Demand
import Definitions.Def_VeinottWagnerSS_RenewalCost_RenewalFunctions

Formal statement

namespace VeinottWagnerSS.RenewalCost

/-- Veinott & Wagner (1965), Eq. (9), p. 533: under `0 ≤ α ≤ 1` and `α φ(0) < 1`,
`r_α(d) = ∑_{i=1}^{∞} αⁱ [Φ^{i−1}(d) − Φⁱ(d)] = α − (1 − α) M_α(d)` for `d = 0, 1, ⋯`. -/
theorem eq9_rAlpha_closed_form (D : DemandDist) (α : ℝ) (hα0 : 0 ≤ α) (hα1 : α ≤ 1)
    (hφ0 : α * D.φ 0 < 1) (d : ℕ) :
    rAlpha D.φ α d = α - (1 - α) * MAlpha D.φ α d := by sorry

end VeinottWagnerSS.RenewalCost

Source

Veinott & Wagner, Computing Optimal (s, S) Inventory Policies, Management Sci. 11 (1965), p. 533, Eq. (9)

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

Eq. (9) — rα(d)=α−(1−α)Mα(d)r_\alpha(d) = \alpha - (1 - \alpha) M_\alpha(d)rα​(d)=α−(1−α)Mα​(d)

Eq. (9) — $r_\alpha(d) = \alpha - (1 - \alpha) M_\alpha(d)$