Bounded surprise for chunk systems
DefinitionKServer_chunk_bounded_surpriseFor a chunk system (the induction package of Bubeck–Coester–Rabani's Lemma 6, formalised here as ChunkSystemB) write for the size of the -th chunk and
for the conditional expected remaining size (ChunkSystemB.condRemaining).
This file adds two notions. The window size is the realised total size of the chunks whose index lies in ; it is a random variable.
The bounded-surprise property with parameter asks that, in every branch and for every window,
The point of the definition is the contrast with what is automatic. Conditioning on the time- history, the quantity is exactly the conditional expectation of , so the inequality holds on average with ; bounded surprise upgrades it to a pointwise, branchwise statement with a slack of . It is the natural companion of the slow-decrement property : slow decrement controls how fast the conditional remaining mass can fall, bounded surprise controls how much realised mass a single branch can hide relative to that fall. Both are needed to make the branchwise bookkeeping of a regrouping argument legitimate.
import Mathlib
import Definitions.Def_KServer_chunk_system_b
import Definitions.Def_KServer_chunk_slow_decrement
namespace KServer
variable {X : Type*} [MetricSpace X] {s t : X} {cLo cHi total price : ℝ} {mLo : ℕ}
/-- The **window size** of a chunk system: the total size of the chunks whose
index lies in the window `[a, b)`,
`S_{[a,b)} = Σ_{a ≤ j < b} c_j`.
It is a random variable, and `S_{[0,∞)}` is the total size of the branch. -/
noncomputable def ChunkSystemB.windowSize
(C : ChunkSystemB X s t cLo cHi total price mLo) (a b : ℕ) (ω : C.Ω) : ℝ :=
∑ j ∈ Finset.univ.filter (fun j : Fin C.m => a ≤ (j : ℕ) ∧ (j : ℕ) < b), C.size ω j
/-- The **bounded-surprise property** with parameter `cmax`: along every branch
and across every window of chunk indices, the realised size of the window
exceeds the drop of the conditional expected remaining size across that window
by at most `cmax`,
`S_{[a,b)} ≤ F_a - F_b + cmax` pointwise.
Since `F_a - F_b` is exactly the *expected* size of the window `[a, b)` given
the time-`a` history, the inequality holds automatically in conditional
expectation with `cmax = 0`; bounded surprise demands it in every individual
branch, up to the slack `cmax`. Together with the slow-decrement property it is
what makes the branchwise bookkeeping of a regrouping argument legitimate. -/
def ChunkSystemB.BoundedSurprise
(C : ChunkSystemB X s t cLo cHi total price mLo) (cmax : ℝ) : Prop :=
∀ (a b : ℕ) (ω : C.Ω), a ≤ b →
C.windowSize a b ω ≤ C.condRemaining a ω - C.condRemaining b ω + cmax
end KServer