Prove2Me

Eq. (10) — closed form of the discounted cost f(x∣s,S)f(x \mid s, S) of a stationary (s,S)(s, S) policy

Proved
VeinottWagnerSS.RenewalCost.eq10_fCost_closed_form

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≤α<10 \le \alpha < 1, K≥0K \ge 0, Gα:Z→RG_\alpha : \mathbb Z \to \mathbb R, and integers s≤Ss \le S with D=S−sD = S - s. The total expected discounted cost of the stationary (s,S)(s, S) policy started from stock xx is

f(x)={Lα(S,D)+K1−rα(D)x<s,Lα(x,x−s)+Lα(S,D)+K1−rα(D) rα(x−s)x≥s.f(x) = \begin{cases} \dfrac{L_\alpha(S, D) + K}{1 - r_\alpha(D)} & x < s, \\[2ex] L_\alpha(x, x - s) + \dfrac{L_\alpha(S, D) + K}{1 - r_\alpha(D)}\, r_\alpha(x - s) & x \ge s. \end{cases}

It expresses the infinite-horizon cost of any (s,S)(s, S) policy through finitely computable renewal quantities.

Formalization Note The denominator 1−rα(D)=(1−α)(1+Mα(D))1 - r_\alpha(D) = (1-\alpha)(1 + M_\alpha(D)) is positive for α<1\alpha < 1; the statement does not rely on Lean's convention y/0=0y/0 = 0. x−sx - s and DD are passed as natural numbers via toNat. No convexity or coercivity of Gα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), Eq. (10), p. 534: for `0 ≤ α < 1`, `K ≥ 0`, integers `s ≤ S` and
`D = S − s`, the discounted cost of the stationary `(s, S)` policy is
`f(x) = (L_α(S, D) + K)/(1 − r_α(D))` for `x < s` and
`f(x) = L_α(x, x − s) + [(L_α(S, D) + K)/(1 − r_α(D))] r_α(x − s)` for `x ≥ s`. -/
theorem eq10_fCost_closed_form (D : DemandDist) (α K : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1)
    (hK : 0 ≤ K) (G : ℤ → ℝ) (s S : ℤ) (hsS : s ≤ S) (x : ℤ) :
    fCost D α K G s S x =
      if x < s then
        (LAlpha D.φ α G S (S - s).toNat + K) / (1 - rAlpha D.φ α (S - s).toNat)
      else
        LAlpha D.φ α G x (x - s).toNat
          + (LAlpha D.φ α G S (S - s).toNat + K) / (1 - rAlpha D.φ α (S - s).toNat)
            * rAlpha D.φ α (x - s).toNat := by sorry

end VeinottWagnerSS.RenewalCost
Source
Veinott & Wagner, Computing Optimal (s, S) Inventory Policies, Management Sci. 11 (1965), p. 534, Eq. (10)
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