Proof of Theorem 3.6, (III): once $\phi$ is zero it stays zero

Proved

StatefulPricing.thm_3_6_proof_III

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamic-resource-allocationonline-learningp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1posted-pricingregret

Consider a run of the chasing oracle of Theorem 3.4 on a DRACC instance with arbitrary valuations, ties broken by an injective rank, a feasible target policy, any initial inventory and any outcome of the coins. If $\phi(t)=0$ for some $t_{\mathrm{init}}\le t\le t_{\mathrm{final}}$ , then

\phi(t')=0\qquad\text{for all } t<t'\le t_{\mathrm{final}}.

Since $\phi(t)=0$ means $\mathrm{Bad}_t=\emptyset$ , there are no Missing rounds after that point.

Differences from the source:

generalization: ties broken by the lexicographic order on $A_t$ → ties broken by an arbitrary injective rank on bundles; reason: every lexicographic order is induced by an injective rank, so the statement specializes to the source's
encoding: random coins of the oracle, $\hat\lambda_{t_{\mathrm{init}}}$ an inventory vector on $A_{t_{\mathrm{init}}}$ → the coin outcomes are an arbitrary fixed sequence and $\hat\lambda_{t_{\mathrm{init}}}$ an arbitrary function $\mathbb N\to\mathbb N$ ; reason: the claim holds for every coin outcome; values off $A_{t_{\mathrm{init}}}$ are never read
encoding: resources $[N]$ , vectors indexed by $A_t$ , prices in $(0,1]^{A_t}$ → resources are a finite set of natural numbers, inventory vectors $\mathbb N\to\mathbb N$ equal to $0$ off $A_t$ , price vectors $\mathbb N\to\mathbb R$ with values in $(0,1]$ at every resource; reason: changes no demand set, payment or inventory

Preamble

import Mathlib
import Definitions.Def_StatefulPricing_Instance
import Definitions.Def_StatefulPricing_Chase

set_option autoImplicit false

open MeasureTheory ProbabilityTheory

Formal statement

namespace StatefulPricing

/-- **(III) of the proof of Theorem 3.6** (arXiv:2005.01869v2, p.10): "(III) if φ(t) = 0 for some
tinit ≤ t ≤ tfinal, then φ(t′) = 0 for all t < t′ ≤ tfinal."

For arbitrary valuations, ties broken by an injective rank, a feasible target policy, any initial
inventory and coin outcomes. -/
theorem thm_3_6_proof_III {T C W : ℕ} (c : Chase T C W) (hrank : Function.Injective c.rank)
    (hγ : IsFeasiblePolicy c.γ) (tfinal : ℕ) :
    ∀ t, c.tinit ≤ t → t ≤ tfinal → c.phi t = 0 →
      ∀ t', t < t' → t' ≤ tfinal → c.phi t' = 0 := by sorry

end StatefulPricing

Source

Emek, Lavi, Niazadeh, Shi, Stateful Posted Pricing with Vanishing Regret via Dynamic Deterministic Markov Decision Processes, arXiv:2005.01869v2, proof of Theorem 3.6, (III), p.10

Human review

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

View graph

Proof of Theorem 3.6, (III): once ϕ\phiϕ is zero it stays zero

Proof of Theorem 3.6, (III): once $\phi$ is zero it stays zero