Chunk padding with the recursion invariants

Proved

KServer.chunk_pad3

by Shuze Chen · Sep 1, 2026 · Mathlib c5ea003 (Lean v4.30.0)

chunk-systemk-serverlower-boundsonline-algorithmsprobability

Chunk padding carrying the full recursion invariants: any chunk system with sizes in $[0, c_B]$ , a trivial initial history, total-variance at most $V$ , L1-sturdiness (expected Doob drawdown of the total at most $D$ at depths up to $n_0$ ), and expected below-floor chunk counts at most $B$ at depths up to $n_0$ , can be modified so that every chunk is nonempty, preserving the chunk count exactly and all of the listed invariants. The padding replaces empty chunks by a repeat of the last consumed request set and does not change the sample space, measure, filtration, or sizes, so every invariant transfers verbatim.

Preamble

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_chunk_adjust
import Definitions.Def_KServer_sturdy

Formal statement

namespace KServer

theorem chunk_pad3 {X : Type*} [MetricSpace X] {s t : X} {cB T pe : ℝ}
    {mL : ℕ} (C : ChunkSystemB X s t 0 cB T pe mL)
    {V D B flo : ℝ} {n₀ : ℕ}
    (hpe0 : 0 ≤ pe)
    (h0triv : ∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂)
    (hVar : ∑ ω, C.P ω * ((∑ i, C.size ω i)
      - ∑ ω', C.P ω' * ∑ i, C.size ω' i) ^ 2 ≤ V)
    (hst : C.SturdyL1 n₀ D)
    (hbad : ∀ n ≤ n₀, ∑ ω, C.P ω * (∑ i ∈ Finset.range n,
        if C.sizeN i ω < flo then (1 : ℝ) else 0) ≤ B) :
    ∃ C' : ChunkSystemB X s t 0 cB T pe mL,
      C'.m = C.m ∧
      (∀ ω₁ ω₂ : C'.Ω, C'.hist 0 ω₁ = C'.hist 0 ω₂) ∧
      (∑ ω, C'.P ω * ((∑ i, C'.size ω i)
          - ∑ ω', C'.P ω' * (∑ i, C'.size ω' i)) ^ 2 ≤ V) ∧
      (∀ (ω : C'.Ω) (i : Fin C'.m), C'.chunk ω i ≠ []) ∧
      C'.SturdyL1 n₀ D ∧
      (∀ n ≤ n₀, ∑ ω, C'.P ω * (∑ i ∈ Finset.range n,
          if C'.sizeN i ω < flo then (1 : ℝ) else 0) ≤ B) := by
  sorry

end KServer

Source

Bansal-Cohen-Ravi style randomized k-server lower bound: level recursion plumbing

View graph