Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

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

Proved
VeinottWagnerSS.Selection.f_below_s

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 < 10≤α<1 and let s≤Ss \le Ss≤S be integers. In the inventory model with set-up cost K≥0K \ge 0K≥0, one-period cost GαG_\alphaGα​ (convex, Gα(y)→∞G_\alpha(y) \to \inftyGα​(y)→∞ as ∣y∣→∞|y| \to \infty∣y∣→∞) and i.i.d. integer demands with finite mean, let f(x∣s,S)f(x \mid s, S)f(x∣s,S) be the expected total discounted cost of the stationary (s,S)(s, S)(s,S) policy started at X1=xX_1 = xX1​=x. If the initial stock is below the reorder point, x<sx < sx<s, then

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

Starting below sss, the policy immediately orders up to SSS; the identity says that the cost of such a start is the set-up cost plus the cost of starting at SSS. In particular aα(x∣s,S)=(1−α)f(x∣s,S)a_\alpha(x \mid s, S) = (1-\alpha)f(x \mid s, S)aα​(x∣s,S)=(1−α)f(x∣s,S) is constant on x<sx < sx<s, which is what makes the function Lα(S,D)\mathcal L_\alpha(S, D)Lα​(S,D) of the paper well defined.

Formalization Note fff is the expected discounted cost of the (s,S)(s,S)(s,S) Markov chain (definition fCost), not a formula; the model's standing assumptions are fields of Model although this identity does not use convexity or coercivity.

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

/-- Veinott & Wagner (1965), §3, p. 533: for `0 ≤ α < 1` and a stationary `(s, S)` policy
(`s ≤ S`), if `X₁ = x < s` then `f(x | s, S) = K + f(S | s, S)`. -/
theorem f_below_s (M : Model) (α : ℝ) (hα0 : 0 ≤ α) (hα1 : α < 1)
    (s S : ℤ) (hsS : s ≤ S) (x : ℤ) (hx : x < s) :
    fCost M α s S x = M.K + fCost M α s S S := by sorry

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me