Prove2Me

Eq. (4): qt=(1+L/p)Dt−1−(L/p)Dt−p−1+z(σ^etL−σ^e,t−1L)q_t = (1 + L/p)D_{t-1} - (L/p)D_{t-p-1} + z(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1})

Proved
ChenBullwhip.Centralized.eq_4

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

bullwhip-effectinventoryp2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1supply-chain

For the retailer's moving-average order-up-to policy with window p≥1p \ge 1, lead-time parameter LL, safety factor zz and constant CL,ρC_{L,\rho}, the order qt=yt−yt−1+Dt−1q_t = y_t - y_{t-1} + D_{t-1} satisfies, for every period tt and every outcome,

qt=L(Dt−1−Dt−p−1p)+Dt−1+z(σ^etL−σ^e,t−1L)=(1+Lp)Dt−1−Lp Dt−p−1+z(σ^etL−σ^e,t−1L).(4)q_t = L\left(\frac{D_{t-1} - D_{t-p-1}}{p}\right) + D_{t-1} + z(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1}) = \left(1 + \frac{L}{p}\right)D_{t-1} - \frac{L}{p}\,D_{t-p-1} + z(\hat\sigma^L_{et} - \hat\sigma^L_{e,t-1}). \tag{4}

The two moving averages D^tL\hat D^L_t and D^t−1L\hat D^L_{t-1} share all but their first and last terms. The identity reduces the order to two demands pp periods apart plus a safety-stock correction, and it is the starting point of the variance computation behind Theorem 2.2.

Formalization Note This is a pathwise identity: it holds for every outcome ω\omega and its proof uses no distributional fact. The demand model is on a probability space. L/pL/p is real division and p≥1p \ge 1 is assumed.

Preamble
import Mathlib
import Definitions.Def_ChenBullwhip_Centralized_AR1Demand
import Definitions.Def_ChenBullwhip_Centralized_Policy
Formal statement
namespace ChenBullwhip.Centralized

theorem eq_4 {Ω : Type*} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω}
    [MeasureTheory.IsProbabilityMeasure P]
    (X : AR1Demand P) (C z : ℝ) (L p : ℕ) (hp : 1 ≤ p) (t : ℤ) (ω : Ω) :
    X.order C z L p t ω
        = (L : ℝ) * ((X.D (t - 1) ω - X.D (t - p - 1) ω) / p) + X.D (t - 1) ω
          + z * (X.sigmaHat C p t ω - X.sigmaHat C p (t - 1) ω)
      ∧ X.order C z L p t ω
        = (1 + (L : ℝ) / p) * X.D (t - 1) ω - ((L : ℝ) / p) * X.D (t - p - 1) ω
          + z * (X.sigmaHat C p t ω - X.sigmaHat C p (t - 1) ω) := by sorry

end ChenBullwhip.Centralized
Source
Chen, Drezner, Ryan and Simchi-Levi, Quantifying the Bullwhip Effect in a Simple Supply Chain, Management Science 46 (2000), p. 438, Eq. (4)
Human review

  • Endorsed by Shuze Chen · Oct 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph