Prove2Me

Theorem 1 — two (s, S) policies with equal average cost below s′s' have equal average cost everywhere

Proved
VeinottWagnerSS.Selection.theorem1_aCost_eq_of_eq_below

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

inventorymarkov-chainp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1ss-policy

Let 0≤α<10 \le \alpha < 1 and consider two stationary (s,S)(s, S) policies (s,S)(s, S) and (s′,S′)(s', S') (so s≤Ss \le S, s′≤S′s' \le S') with s≤s′s \le s'. Let aα(x∣s,S)=(1−α)f(x∣s,S)a_\alpha(x \mid s, S) = (1-\alpha) f(x \mid s, S) be the equivalent average cost per period from the starting stock X1=xX_1 = x. If

aα(x∣s,S)=aα(x∣s′,S′)for all x<s′,a_\alpha(x \mid s, S) = a_\alpha(x \mid s', S') \qquad \text{for all } x < s',

then

aα(x∣s,S)=aα(x∣s′,S′)for all integers x.a_\alpha(x \mid s, S) = a_\alpha(x \mid s', S') \qquad \text{for all integers } x.

The theorem reduces the comparison of two policies on all starting stocks to the comparison on the finitely many stocks s≤x<s′s \le x < s' that matter in Step iii of the paper's algorithm, and it is one of the two ingredients of Theorem 2.

Formalization Note The model's standing assumptions (convexity and coercivity of GαG_\alpha, K≥0K \ge 0, finite mean demand) are fields of Model; the statement is kept under them as in the paper, although it does not need them.

Preamble
import Mathlib
import Definitions.Def_VeinottWagnerSS_Selection_Model
Formal statement
namespace VeinottWagnerSS.Selection

/-- Veinott & Wagner (1965), Theorem 1, p. 542: if `0 ≤ α < 1`, if the two `(s, S)` policies
`(s, S)`, `(s', S')` satisfy `s ≤ s'`, and if `a_α(x | s, S) = a_α(x | s', S')` for every
`x < s'`, then `a_α(x | s, S) = a_α(x | s', S')` for all `x`. -/
theorem theorem1_aCost_eq_of_eq_below (M : Model) (α : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1)
    (s S s' S' : ℤ) (hsS : s ≤ S) (hsS' : s' ≤ S') (hss' : s ≤ s')
    (heq : ∀ x : ℤ, x < s' → aCost M α s S x = aCost M α s' S' x) :
    ∀ x : ℤ, aCost M α s S x = aCost M α s' S' x := by sorry

end VeinottWagnerSS.Selection
Source
Veinott & Wagner, Computing Optimal (s, S) Inventory Policies, Management Sci. 11 (1965), p. 542, Theorem 1 (proof: Appendix §3, pp. 550-551)
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