Prove2Me

Appendix D, Proof of Theorem 1, p. 35 — at n = N, E[ℋ_N] = min over K^N ≤ K̄ − ζ^N_N of E[ℋ^s(K^N, ·)]

Proved
OnDemandDelivery.Approx.last_period

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

approximationdynamic-programmingp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Consider the dispatching and routing model under its standing assumptions and a driver status ζN\zeta^N in the last period with ζNN≤Kˉ\zeta^N_N \le \bar K. Then the expected last-period cost-to-go equals the best expected single-period cost over the admissible numbers of dispatched drivers:

EQN[HN(IN,qN,ζN)]=min⁡KN∈N, KN≤Kˉ−ζNNEQN[Hs(KN,IN,qN)].\mathbb E_{\mathbb Q^N}\big[\mathcal H_N(\mathcal I^N, q^N, \zeta^N)\big] = \min_{K^N \in \mathbb N,\ K^N \le \bar K - \zeta^N_N} \mathbb E_{\mathbb Q^N}\big[\mathcal H^s(K^N, \mathcal I^N, q^N)\big].

The right-hand side is the problem APTN(ζN)\mathbf{APT}^N(\zeta^N), so this identity is the exactness of the approximation in the last period. Its content is that the minimum over the number of drivers may be taken outside the expectation, since in the last period it is optimal to use every available driver.

Formalization Note. HN\mathcal H_N is defined directly by (8), as a minimum over single-period decisions feasible with Kˉ−ζNN\bar K - \zeta^N_N available drivers, not through the right-hand side. Values are in [0,∞][0,\infty]; the minimum on the right is an infimum over KN∈NK^N \in \mathbb N with KN≤Kˉ−ζNNK^N \le \bar K - \zeta^N_N as real numbers.

Preamble
import Mathlib
import Definitions.Def_OnDemandDelivery_Approx_Setting

open scoped ENNReal NNReal
Formal statement
namespace OnDemandDelivery.Approx
open Model
theorem last_period {L : Type*} [Fintype L] (M : Model L) (hM : M.Standing) (ζ : ℕ → ℕ)
    (hζ : ζ M.N ≤ M.Kbar) :
    M.EH M.N ζ = ⨅ (K : ℕ) (_ : (K : ℝ) ≤ (M.Kbar : ℝ) - (ζ M.N : ℝ)), M.EHs M.N K := by sorry
end OnDemandDelivery.Approx
Source
Liu, Luo, On-Demand Delivery from Stores: Dynamic Dispatching and Routing with Random Demand, arXiv:2107.13058v3, p. 35, Appendix D, Proof of Theorem 1, display after "Lastly, when n = N"
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