Prove2Me

§4, p. 537 — S‾\underline{S} exists and is the unique integer with ΔGα(S‾−1)<0≤ΔGα(S‾)\Delta G_\alpha(\underline{S}-1) < 0 \le \Delta G_\alpha(\underline{S})

Proved
VeinottWagnerSS.Bounds.SLow_characterization

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

inventoryp2o-batch-p200bp2o-gran-per-chapterp2o-plan-paperp2o-v1ss-policy

Let Gα:Z→RG_\alpha : \mathbb Z \to \mathbb R be convex on the integers, i.e. its forward differences ΔGα(y)=Gα(y+1)−Gα(y)\Delta G_\alpha(y) = G_\alpha(y+1) - G_\alpha(y) are non-decreasing in yy, and suppose Gα(y)→∞G_\alpha(y) \to \infty as y→+∞y \to +\infty and as y→−∞y \to -\infty. Let K≥0K \ge 0 and 0≤α≤10 \le \alpha \le 1. Then the set of integers minimizing GαG_\alpha has a least element, namely S‾\underline{S}, and an integer yy satisfies

ΔGα(y−1)<0≤ΔGα(y)\Delta G_\alpha(y - 1) < 0 \le \Delta G_\alpha(y)

if and only if y=S‾y = \underline{S}.

This is the characterization of S‾\underline{S} given on p. 537 of Veinott and Wagner (1965); it identifies the order-up-to level of the single-period problem and is the anchor of all four bounds (21)–(23).

Formalization Note The hypotheses on KK and α\alpha are the paper's standing assumptions and are not used by this statement. ΔGα(y−1)\Delta G_\alpha(y-1) is written G y - G (y - 1).

Preamble
import Mathlib
import Definitions.Def_VeinottWagnerSS_Bounds_CriticalNumbers
Formal statement
namespace VeinottWagnerSS.Bounds

/-- p. 537: under the standing assumptions (`G_α` convex on `ℤ` and `G_α(y) → ∞` as
`|y| → ∞`), `S̲ = SLow G` is the smallest integer minimizing `G_α`, and it is the unique
integer `y` with `ΔG_α(y − 1) < 0 ≤ ΔG_α(y)`, where `ΔG_α(y) = G_α(y + 1) − G_α(y)`. -/
theorem SLow_characterization (G : ℤ → ℝ) (K α : ℝ) (hα₀ : 0 ≤ α) (hα₁ : α ≤ 1) (hK : 0 ≤ K)
    (hconv : ∀ y : ℤ, G (y + 1) - G y ≤ G (y + 2) - G (y + 1))
    (hG_top : Filter.Tendsto G Filter.atTop Filter.atTop)
    (hG_bot : Filter.Tendsto G Filter.atBot Filter.atTop) :
    IsLeast {y : ℤ | ∀ z : ℤ, G y ≤ G z} (SLow G) ∧
      ∀ y : ℤ, (G y - G (y - 1) < 0 ∧ 0 ≤ G (y + 1) - G y ↔ y = SLow G) := by sorry

end VeinottWagnerSS.Bounds
Source
Veinott & Wagner, Computing Optimal (s, S) Inventory Policies, Management Sci. 11 (1965), p. 537, Section 4 'Bounds on s* and S*', definition of S underbar and display ΔG_α(S̲ − 1) < 0 ≤ ΔG_α(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