Proposition 2 — Finite-cap policy cost bound
ProvedCappedBaseStock.finite_cap_cost_boundConsider a periodic-review lost-sales inventory system. Demand is i.i.d., nonnegative and real-valued, with . Lead time is an integer , and holding and lost-sales rates satisfy . Inventory and the pipeline coordinates initially equal zero. The first pipeline component arrives, the order is placed before current demand is observed, demand is served up to available inventory, and the remaining pipeline shifts; today's order arrives periods later. The period cost is .
Costs use the upper limit of finite-horizon expected average costs from this empty initial state. is the infimum over all measurable, possibly time-dependent history policies in the canonical demand-path model, with independent uniform private randomization. Infinite expected costs remain infinite. A capped base-stock rule orders , with finite . Its cost is denoted by , and is the infimum over these parameters. Ordinary base stock at level is the same rule with cap .
For a demand block, let , including the zero empty sum. A pair is feasible when , , and, for both and ,
The lower certificate is the infimum of over this feasible set. Neither attainment of the infimum nor positivity of is assumed. Claim. For every feasible pair , choose and cap . Then
This target is the cost conclusion of Proposition 2, equation eq-finite-cap-bound. Its other stationary shortfall inequalities are not asserted here. The cost in the conclusion is the original zero-start long-run cost, so any stationary argument used in its proof must be connected to that objective.
import Definitions.Def_CappedBaseStock_Model open scoped ENNReal
namespace CappedBaseStock
theorem finite_cap_cost_bound (P : DemandLaw) (c : Parameters) (r z : ℝ)
(feasible : CertificateFeasible P c r z) :
cbsCost P c (Real.toNNReal (((c.L : ℝ) + 1) * r + z)) (Real.toNNReal r) ≤
ENNReal.ofReal ((c.h + c.p / ((c.L : ℝ) + 1)) * z +
(2 - 1 / ((c.L : ℝ) + 1)) * c.p * (mean P - r)) := by sorry
end CappedBaseStockRead-back
What the Lean code literally says, in plain math · GPT-6 (independent Codex sub-agent)
For every probability measure on the nonnegative real numbers with integrable identity function and strictly positive real mean , every integer , every pair of real numbers and , and all real numbers satisfying the following feasibility conditions, the stated cost bound holds. For every nonnegative real demand sequence and integer , write , where contributes the empty sum , and , with . Feasibility means exactly , , and for both and ; these are nonnegative Lebesgue integrals and inequalities in the extended nonnegative reals , with the positive parts and the finite right sides embedded into that space. Set and , both finite nonnegative real numbers; the feasibility conditions make these equal to and . Let have the infinite independent product law , and independently let have law equal to Lebesgue measure restricted to . Starting with and for every , use and the recursion , for , and for every integer . This recursion does not use , although its cost is integrated over the stated joint law. Define as an extended nonnegative real and , where ranges over nonnegative integers and each integral is a nonnegative Lebesgue integral. The assertion is , with the finite right side embedded in ; it is already nonnegative under the hypotheses. All subtractions shown inside positive parts are truncated at zero, whereas the sums in and the expression inside use ordinary real subtraction. The average cost uses extended nonnegative arithmetic and can in its definition equal ; its denominator is the positive finite number . This is a bound for the specified pair , with no infimum or assertion of optimality or attainment. The quantifiers include , zero demand values, , , and when feasible, and ensures that is nonzero.
Confirmed by the mission captain (proposal self-audit).