Lemma 1(i), p. 12 — the cost-to-go ℋ_n(ℐ^n, q^n, ζ^n) is nondecreasing in the driver status ζ^n

Proved

OnDemandDelivery.Approx.lemma_1_i

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

dynamic-programmingmonotonicityp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Consider the dispatching and routing model under its standing assumptions and a period $1 \le n \le N$ . For every realized demand $(\mathcal I^n, q^n)$ and driver statuses $\zeta^n_1, \zeta^n_2$ with $\zeta^n_1 \ge \zeta^n_2$ componentwise,

\mathcal H_n(\mathcal I^n, q^n, \zeta^n_1) \ge \mathcal H_n(\mathcal I^n, q^n, \zeta^n_2).

More drivers en route can only increase the optimal expected cost; this is the structural property the approximation APT is designed to share (part (ii) of the lemma).

Formalization Note. " $\zeta^n_1 \ge \zeta^n_2$ " is the componentwise order on status vectors indexed by all periods. Values are in $[0,\infty]$ .

Preamble

import Mathlib
import Definitions.Def_OnDemandDelivery_Approx_Setting

open scoped ENNReal NNReal

Formal statement

namespace OnDemandDelivery.Approx
open Model
theorem lemma_1_i {L : Type*} [Fintype L] (M : Model L) (hM : M.Standing) (n : ℕ)
    (hn : 1 ≤ n) (hnN : n ≤ M.N) (d : Demand L) (ζ₁ ζ₂ : ℕ → ℕ) (h : ζ₂ ≤ ζ₁) :
    M.H n d ζ₂ ≤ M.H n d ζ₁ := by sorry
end OnDemandDelivery.Approx

Source

Liu, Luo, On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand, arXiv:2107.13058v3, p. 12, Lemma 1(i)

Human review

Endorsed by Shuze Chen · Oct 16, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 16, 2026
Confirmed by the mission captain (proposal self-audit).

View graph