Eq. (8) — $L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)\, m_\alpha(j)$

Proved

VeinottWagnerSS.RenewalCost.eq8_LAlpha_interchange

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, $0 \le \alpha \le 1$ with $\alpha\varphi(0) < 1$ , and $G_\alpha : \mathbb Z \to \mathbb R$ arbitrary. For every integer $x$ and every $d = 0, 1, \dots$ , the double series (7) defining $L_\alpha(x, d)$ converges absolutely, and interchanging the order of summation gives

L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)\, m_\alpha(j),

where $m_\alpha(j) = \sum_{i \ge 1} \alpha^i \varphi^i(j)$ .

This finite form is what makes $L_\alpha$ computable once $m_\alpha$ is known.

Formalization Note Absolute convergence is stated as summability over $i$ of $\sum_{k=0}^{d} |\alpha^i G_\alpha(x-k)\varphi^i(k)|$ (the inner sum is finite). $L_\alpha$ is defined by the series (7).

Preamble

import Mathlib
import Definitions.Def_VeinottWagnerSS_RenewalCost_Demand
import Definitions.Def_VeinottWagnerSS_RenewalCost_RenewalFunctions

Formal statement

namespace VeinottWagnerSS.RenewalCost

/-- Veinott & Wagner (1965), Eq. (8), p. 533: under `0 ≤ α ≤ 1` and `α φ(0) < 1`, the double
series (7) defining `L_α(x, d)` converges absolutely, and interchanging the order of summation
gives `L_α(x, d) = G_α(x) + ∑_{j=0}^{d} G_α(x − j) m_α(j)`. -/
theorem eq8_LAlpha_interchange (D : DemandDist) (α : ℝ) (hα0 : 0 ≤ α) (hα1 : α ≤ 1)
    (hφ0 : α * D.φ 0 < 1) (G : ℤ → ℝ) (x : ℤ) (d : ℕ) :
    Summable (fun i : ℕ => ∑ k ∈ Finset.range (d + 1),
        |α ^ (i + 1) * G (x - (k : ℤ)) * convPow D.φ (i + 1) k|) ∧
      LAlpha D.φ α G x d =
        G x + ∑ j ∈ Finset.range (d + 1), G (x - (j : ℤ)) * mAlpha D.φ α j := by sorry

end VeinottWagnerSS.RenewalCost

Source

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

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. (8) — Lα(x,d)=Gα(x)+∑j=0dGα(x−j) mα(j)L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)\, m_\alpha(j)Lα​(x,d)=Gα​(x)+∑j=0d​Gα​(x−j)mα​(j)

Eq. (8) — $L_\alpha(x, d) = G_\alpha(x) + \sum_{j=0}^{d} G_\alpha(x - j)\, m_\alpha(j)$