Finite-cap construction: average inventory bound
ProvedCappedBaseStock.finite_cap_inventory_boundConsider the canonical periodic-review lost-sales model with i.i.d. nonnegative demand of finite positive mean, positive integer lead time, and positive holding and penalty rates. Begin with zero on-hand inventory and an empty pipeline. Fix a feasible certificate pair:
where the finite maximum includes the empty sum:
Run the capped base-stock policy with finite parameters
The expected Cesàro average of post-demand inventory satisfies
The upper limit is taken in the extended nonnegative reals. This is an inventory-moment bound, with no holding-cost coefficient. It requires neither an invariant initial distribution nor convergence to a unique stationary law, and it includes zero cap and zero certificate inventory.
This moment estimate isolates the inventory component of Proposition 2 and can be reused with any positive holding-cost rate. It is the zero-initial-state, long-run formulation of the inventory estimate in the manuscript’s finite-cap argument.
import Definitions.Def_CappedBaseStock_Model open scoped ENNReal
namespace CappedBaseStock
theorem finite_cap_inventory_bound (P : DemandLaw) (c : Parameters) (r z : ℝ)
(feasible : CertificateFeasible P c r z) :
averageCost P (fun t ω =>
((cbsRun c (Real.toNNReal (((c.L : ℝ) + 1) * r + z))
(Real.toNNReal r) ω (t + 1)).1 : ℝ≥0∞)) ≤ ENNReal.ofReal z := by sorry
end CappedBaseStock