§3, p. 533 — $f(x) = K + f(S)$ for $x < s$

Proved

VeinottWagnerSS.RenewalCost.f_below_s

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

inventoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1ss-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 < s$ , its total expected discounted cost is

f(x \mid s, S) = K + f(S \mid s, S).

Below $s$ the policy orders immediately up to $S$ , paying the set-up cost $K$ , and thereafter behaves as if started at $S$ .

Formalization Note $f$ is the expected cost of the controlled chain (definition fCost). 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) = K + f(S)`. -/
theorem f_below_s (D : DemandDist) (α K : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1) (hK : 0 ≤ K)
    (G : ℤ → ℝ) (s S : ℤ) (hsS : s ≤ S) (x : ℤ) (hx : x < s) :
    fCost D α K G s S x = K + fCost D α K G s S S := by sorry

end VeinottWagnerSS.RenewalCost

Source

Veinott & Wagner, Computing Optimal (s, S) Inventory Policies, Management Sci. 11 (1965), p. 533, §3, display f(x) = K + f(S), 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)=K+f(S)f(x) = K + f(S)f(x)=K+f(S) for x<sx < sx<s

§3, p. 533 — $f(x) = K + f(S)$ for $x < s$