§3, p. 533 — $f(x) = L_\alpha(x, x-s) + K r_\alpha(x-s) + f(S) r_\alpha(x-s)$ for $x \ge s$

Proved

VeinottWagnerSS.RenewalCost.f_above_s

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

inventoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1renewal-theoryss-policy

Let $\varphi$ be a demand distribution, $0 \le \alpha < 1$ , $K \ge 0$ , $G_\alpha : \mathbb Z \to \mathbb R$ , and integers $s \le S$ . If the stationary $(s, S)$ policy is started from stock $x \ge s$ , its total expected discounted cost satisfies

f(x) = L_\alpha(x, x - s) + K r_\alpha(x - s) + f(S)\, r_\alpha(x - s).

No order is placed until cumulative demand exceeds $x - s$ ; then an order up to $S$ is placed and the process renews.

Formalization Note $x - s \ge 0$ is passed to $L_\alpha$ and $r_\alpha$ as a natural number ((x - s).toNat, exact because $s \le x$ ). $f$ is the expected cost of the controlled chain. No convexity or coercivity of $G_\alpha$ is assumed.

Preamble

import Mathlib
import Definitions.Def_VeinottWagnerSS_RenewalCost_Demand
import Definitions.Def_VeinottWagnerSS_RenewalCost_RenewalFunctions
import Definitions.Def_VeinottWagnerSS_RenewalCost_PolicyCost

Formal statement

namespace VeinottWagnerSS.RenewalCost

/-- Veinott & Wagner (1965), §3, p. 533: for `0 ≤ α < 1`, `K ≥ 0` and integers `s ≤ S`, if
`X₁ = x ≥ s` then `f(x) = L_α(x, x − s) + K r_α(x − s) + f(S) r_α(x − s)`. -/
theorem f_above_s (D : DemandDist) (α K : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1) (hK : 0 ≤ K)
    (G : ℤ → ℝ) (s S : ℤ) (hsS : s ≤ S) (x : ℤ) (hx : s ≤ x) :
    fCost D α K G s S x =
      LAlpha D.φ α G x (x - s).toNat + K * rAlpha D.φ α (x - s).toNat
        + fCost D α K G s S S * rAlpha D.φ α (x - s).toNat := by sorry

end VeinottWagnerSS.RenewalCost

Source

Veinott & Wagner, Computing Optimal (s, S) Inventory Policies, Management Sci. 11 (1965), p. 533, §3, last display (x ≥ s)

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

§3, p. 533 — f(x)=Lα(x,x−s)+Krα(x−s)+f(S)rα(x−s)f(x) = L_\alpha(x, x-s) + K r_\alpha(x-s) + f(S) r_\alpha(x-s)f(x)=Lα​(x,x−s)+Krα​(x−s)+f(S)rα​(x−s) for x≥sx \ge sx≥s

§3, p. 533 — $f(x) = L_\alpha(x, x-s) + K r_\alpha(x-s) + f(S) r_\alpha(x-s)$ for $x \ge s$