Finite-cap construction: average lost-sales bound
ProvedCappedBaseStock.finite_cap_lost_sales_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
Writing the lost sales in period t as the positive part of demand minus available inventory, the expected Cesàro average obeys
The upper limit is taken in the extended nonnegative reals. This is a lost-sales-moment bound, with no penalty-cost coefficient. It covers both endpoint caps and zero certificate inventory; no stationary initial law or ergodicity hypothesis is assumed.
This moment estimate isolates the lost-sales component of Proposition 2 and can be reused with any positive penalty rate. It is the zero-initial-state, long-run formulation of the lost-sales estimate resulting from the manuscript’s finite-cap argument.
import Definitions.Def_CappedBaseStock_Model open scoped ENNReal
namespace CappedBaseStock
theorem finite_cap_lost_sales_bound (P : DemandLaw) (c : Parameters) (r z : ℝ)
(feasible : CertificateFeasible P c r z) :
averageCost P (fun t ω =>
(lostSales c (cbsRun c (Real.toNNReal (((c.L : ℝ) + 1) * r + z))
(Real.toNNReal r) ω t) (ω.1 t) : ℝ≥0∞)) ≤
ENNReal.ofReal ((mean P - r) +
(z + (c.L : ℝ) * (mean P - r)) / ((c.L : ℝ) + 1)) := by sorry
end CappedBaseStock