Tame subchunk systems for the BCR level induction

Definition

KServer_bcr_subchunks_tame

by Gabewhigham · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

k-serveronline-algorithmsprobability

Bubeck-Coester-Rabani's randomized $\\Omega(\\log^2 k)$ lower bound for the $k$ -server problem proceeds by an induction over levels $w$ . Claim 13 turns a level- $w$ chunk system into a system of subchunks on level $w+1$ , with maximal size $\\tfrac32\\cdot 3^{w}$ , escape price $2\\beta 3^{w}$ and expected total $\\alpha\\beta(w+1)^2 3^{w+1}+3\\cdot 3^{w}$ : an extra $3\\cdot 3^{w}$ of expected cost is produced precisely to pay for the loss in the next step.

This file records the same output, made tame: it additionally asks that the conditional expected remaining size $F_h=\\mathbb E[\\sum_{j\\ge h}c_j\\mid\\mathcal F_h]$ of the subchunk system satisfies, in every branch,

F_h-\\tfrac32\\cdot 3^{w}\\le F_{h+1}\\qquad\\text{and}\\qquad \\sum_{a\\le j<b}c_j\\le F_a-F_b+\\tfrac32\\cdot 3^{w}.

Both inequalities hold automatically in conditional expectation, because the current size is measurable at the current time and $F_a-\\mathbb E[F_b\\mid\\mathcal F_a]$ is the conditional expectation of the window size; the tame version demands them branchwise. These are exactly the two properties consumed by the regrouping step of Lemma 15, which cuts the subchunk sequence at the stopping times of $F$ and therefore reasons inside individual branches.

Definition code

import Mathlib
import Definitions.Def_KServer_chunk_slow_decrement
import Definitions.Def_KServer_chunk_bounded_surprise

namespace KServer

/-- The output of Claim 13, made **tame**: the level-`w` subchunk system whose
conditional expected remaining size is both *slowly decreasing* and
*surprise-bounded* with parameter equal to the maximal subchunk size
`3 * 3 ^ w / 2`.  These are the two branchwise properties that the regrouping
step of Lemma 15 consumes; both hold automatically in conditional expectation,
and both are recorded here because the regrouping is a branchwise
stopping-time argument. -/
def BCRInductiveSubchunksTame (α : ℝ) (β : ℕ) (hβ : 0 < β) (w : ℕ) : Prop :=
  ∃ C : @ChunkSystemB (bcrLevel2 β hβ (w + 1)).carrier
      (bcrLevel2 β hβ (w + 1)).metric
      (bcrLevel2 β hβ (w + 1)).s (bcrLevel2 β hβ (w + 1)).t
      0 (3 * (3 : ℝ) ^ w / 2)
      ((α * β * ((w + 1 : ℕ) : ℝ) ^ 2) * 3 ^ (w + 1) + 3 * (3 : ℝ) ^ w)
      (2 * β * (3 : ℝ) ^ w) 0,
    (∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂) ∧
      C.SlowDecrement (3 * (3 : ℝ) ^ w / 2) ∧
      C.BoundedSurprise (3 * (3 : ℝ) ^ w / 2)

end KServer

Source

Bubeck, Coester, Rabani, Shortest paths without a map, but with an entropic regularizer, arXiv:2211.05753v2, Section 5, Claim 13 and Lemma 15

View graph