§3, p. 533 — for
ProvedVeinottWagnerSS.Selection.f_below_sLet and let be integers. In the inventory model with set-up cost , one-period cost (convex, as ) and i.i.d. integer demands with finite mean, let be the expected total discounted cost of the stationary policy started at . If the initial stock is below the reorder point, , then
Starting below , the policy immediately orders up to ; the identity says that the cost of such a start is the set-up cost plus the cost of starting at . In particular is constant on , which is what makes the function of the paper well defined.
Formalization Note is the expected discounted cost of the 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.
import Mathlib import Definitions.Def_VeinottWagnerSS_Selection_Model
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
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.