Lemma 2 — Greedy recursion on a consecutive block

Proved

CappedBaseStock.greedy_window

by StellaXin · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximationcapped-base-stockinventorylost-salesoperations-research

Fix an integer $L\ge1$ and two nonnegative real sequences $(a_t)_{t\in\mathbb Z}$ and $(b_t)_{t\in\mathbb Z}$ . Suppose that, for every integer $t$ ,

a_t=\left(b_t-\sum_{i=1}^{L}a_{t-i}\right)^+.

Then, for every integer starting index $s$ and every integer length $1\le n\le L+1$ ,

\sum_{j=0}^{n-1}a_{s+j}\le\max_{0\le j<n}b_{s+j}.

The recurrence includes the terms preceding the block; they are not reset to zero at its beginning. Blocks are nonempty so their ordinary finite maximum is defined. No inventory, independence, or expectation hypotheses are needed.

Preamble

import Mathlib

open scoped BigOperators

Formal statement

namespace CappedBaseStock


theorem greedy_window
    (L : ℕ) (hL : 1 ≤ L)
    (a b : ℤ → ℝ)
    (ha : ∀ t : ℤ, 0 ≤ a t)
    (hb : ∀ t : ℤ, 0 ≤ b t)
    (hrec : ∀ t : ℤ,
      a t = max (b t - ∑ i ∈ Finset.Icc 1 L, a (t - (i : ℤ))) 0)
    (start : ℤ) (n : ℕ) (hn : 0 < n) (hlen : n ≤ L + 1) :
    (∑ i ∈ Finset.range n, a (start + (i : ℤ))) ≤
      (Finset.range n).sup'
        (Finset.nonempty_range_iff.mpr (Nat.ne_of_gt hn))
        (fun i => b (start + (i : ℤ))) := by sorry

end CappedBaseStock

Source

Linwei Xin, Capped Base-Stock Policies: A 2.33-Approximation, author-supplied LaTeX manuscript (756 lines); public paper listing https://papers.ssrn.com/sol3/papers.cfm?abstract_id=7134538 . Author-supplied source SHA-256: f353793c255e1ebed5f3ec541037284bd926183e3e5b71941f13e79c2d67cb7a. Lemma 2 (`lem-greedy-window`), lines 502–512.

Read-back

What the Lean code literally says, in plain math · GPT-6 (independent Codex sub-agent)

For every natural number $L$ with $1\le L$ , every pair of functions $a,b:\mathbb Z\to\mathbb R$ satisfying $a(t)\ge0$ and $b(t)\ge0$ for every integer $t$ , and the recurrence $a(t)=\max\{b(t)-\sum_{j=1}^{L}a(t-j),0\}$ for every integer $t$ , every integer $s$ , and every natural number $n$ satisfying $0<n\le L+1$ , one has $\sum_{i=0}^{n-1}a(s+i)\le\max_{0\le i<n}b(s+i)$ . The maximum on the right is the maximum over the finite nonempty set of indices $0,\ldots,n-1$ . The starting index $s$ may be negative, zero, or positive, and the recurrence is required at all integer indices, including indices before the displayed block; its preceding $L$ terms are not truncated at $s$ . The assumptions exclude $L=0$ and $n=0$ , include $L=1$ , $n=1$ , and $n=L+1$ , and permit zero values of either function, including the identically zero pair.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by StellaXin · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph