The chunk-combining lemma: uniform windows from conditional hitting times
ProvedKServer.chunk_combiningThe chunk-combining lemma (the repaired form of Lemma 10 of Bubeck–Coester–Rabani, STOC 2023). Let be a chunk system with online escapes on a metric space with marked points : sizes in with , escape price , trivial initial knowledge ( trivial), and total expected mass . Assume the Doob jump bound in the descending regime: the martingale has pointwise jumps at most . Then for every target count the chunks can be regrouped into windows delimited by the hitting times of the uniformly spaced levels of the conditional future mass , yielding a chunk system with the same outcomes, weights and request sequence, whose conditional window sizes all lie within of the spacing :
for any escape price . The expected total is preserved exactly (the tower property), so the same lower bound carries over. The proof pins the boundary overshoots by one chunk plus one Doob jump (since the conditional future mass descends monotonically, so no up-crossings occur), computes the conditional window sizes by optional stopping, and charges a bailing adversary's untouched window tail — at most one spacing plus slack in conditional expectation — to the price difference , applying the input's conditional cost bound chunkwise on the quiet, still-in-window events, which are measurable in the fine filtration. This is the engine that turns the stage-constructed level- system into the standard windowed form in the induction of Lemma 6.
import Mathlib import Definitions.Def_KServer_evader import Definitions.Def_KServer_evader_bail import Definitions.Def_KServer_chunk_system_b import Definitions.Def_KServer_chunk_cond import Definitions.Def_KServer_chunk_stopping import Definitions.Def_KServer_bail_append
namespace KServer
theorem chunk_combining {X : Type*} [MetricSpace X] {s t : X}
{cA cB T pe : ℝ} {mL : ℕ}
(C : ChunkSystemB X s t cA cB T pe mL)
(h0 : ∀ ω ω' : C.Ω, C.hist 0 ω = C.hist 0 ω')
{jbS : ℝ} (hjb : C.DoobJumpBound jbS) (hjb0 : 0 ≤ jbS) (hjbA : jbS ≤ cA)
(hcA : 0 < cA) (hcAB : cA ≤ cB)
{M : ℕ} (hM0 : 0 < M) {cLo' cHi' p' : ℝ}
(hlo0 : 0 < cLo')
(hlo : cLo' ≤ (∑ ω, C.P ω * ∑ i, C.size ω i) / M - (cB + jbS))
(hhi : (∑ ω, C.P ω * ∑ i, C.size ω i) / M + (cB + jbS) ≤ cHi')
(hp : pe + ((∑ ω, C.P ω * ∑ i, C.size ω i) / M + (cB + jbS)) ≤ p') :
Nonempty (ChunkSystemB X s t cLo' cHi' T p' M) := by sorry
end KServer