Prove2Me

§3, p. 533 — renewal equation f(S)=Lα(S,D)+Krα(D)+f(S)rα(D)f(S) = L_\alpha(S, D) + K r_\alpha(D) + f(S) r_\alpha(D)

Proved
VeinottWagnerSS.RenewalCost.renewal_equation_fS

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. Let f(x)=f(x∣s,S)f(x) = f(x \mid s, S) be the total expected discounted cost of the stationary (s,S)(s, S) policy started from stock xx. Then

f(S)=Lα(S,D)+Krα(D)+f(S) rα(D).f(S) = L_\alpha(S, D) + K r_\alpha(D) + f(S)\, r_\alpha(D).

Starting at SS, no order is placed until cumulative demand exceeds DD, after which the process restarts from SS; the equation expresses this renewal.

Formalization Note ff is the expected cost of the controlled chain (definition fCost), not a closed form. Convexity and coercivity of GαG_\alpha, standing assumptions of the paper, are not assumed: for α<1\alpha < 1 the statement holds for every GαG_\alpha.

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`, with
`D = S − s`, the discounted cost of the stationary `(s, S)` policy started at `X₁ = S`
satisfies the renewal equation `f(S) = L_α(S, D) + K r_α(D) + f(S) r_α(D)`. -/
theorem renewal_equation_fS (D : DemandDist) (α K : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1)
    (hK : 0 ≤ K) (G : ℤ → ℝ) (s S : ℤ) (hsS : s ≤ S) :
    fCost D α K G s S S =
      LAlpha D.φ α G S (S - s).toNat + K * rAlpha D.φ α (S - s).toNat
        + fCost D α K G s S S * rAlpha D.φ α (S - s).toNat := by sorry

end VeinottWagnerSS.RenewalCost
Source
Veinott & Wagner, Computing Optimal (s, S) Inventory Policies, Management Sci. 11 (1965), p. 533, §3 (Renewal Approach), first display after 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