Conditional remaining size and slow decrement for chunk systems
DefinitionKServer_chunk_slow_decrementLet be a chunk system with online escapes (ChunkSystemB, the induction package of Bubeck-Coester-Rabani's Lemma 6): a finitely supported random sequence of chunks of set requests, with an explicit filtration encoded by a history function, adapted chunk sizes , and a conditional cost bound against every evader and every online escape rule.
This file introduces the filtration's atoms - the fibres of the time- history function, which are exactly the cells on which conditioning at time takes place - and the conditional expected remaining size
a random variable that is constant on each time- atom. When the initial information is trivial, is precisely the expected total size of the system, and it therefore dominates the system's declared total.
The slow-decrement property with parameter demands that this quantity never falls fast:
Because the current size is measurable at time , the tower identity always bounds the drop of by in conditional expectation whenever the sizes are bounded by ; the slow-decrement property demands the same bound in each individual branch, which is what a branchwise stopping-time argument actually consumes.
Finally the file records the output shape of the level- subchunk construction of the randomized lower bound with the slow-decrement property attached, so that a regrouping step on the next level can be stated against it.
import Mathlib
import Definitions.Def_KServer_chunk_system_b
import Definitions.Def_KServer_bcr_induction
namespace KServer
variable {X : Type*} [MetricSpace X] {s t : X} {cLo cHi total price : ℝ} {mLo : ℕ}
/-- The time-`h` **atom** of the outcome `ω`: the set of outcomes that share its
history at time `h`. The filtration of a chunk system is encoded by the map
`hist : ℕ → Ω → ℕ`, so the atoms are the fibres of `hist h`. -/
def ChunkSystemB.atom (C : ChunkSystemB X s t cLo cHi total price mLo) (h : ℕ)
(ω : C.Ω) : Finset C.Ω :=
Finset.univ.filter (fun ω' => C.hist h ω' = C.hist h ω)
/-- The **conditional expected remaining size** of a chunk system at time `h`:
the conditional expectation, given the time-`h` history, of the total size of
the chunks with index at least `h`,
`F_h = E[ Σ_{j ≥ h} c_j | hist h ]`.
It is constant on each atom of `hist h`, and `F_0` is the expected total size. -/
noncomputable def ChunkSystemB.condRemaining
(C : ChunkSystemB X s t cLo cHi total price mLo) (h : ℕ) (ω : C.Ω) : ℝ :=
(∑ ω' ∈ C.atom h ω, C.P ω' *
∑ j ∈ Finset.univ.filter (fun j : Fin C.m => h ≤ (j : ℕ)), C.size ω' j)
/ (∑ ω' ∈ C.atom h ω, C.P ω')
/-- The **slow-decrement property** with parameter `cmax`: along every branch and
at every time, the conditional expected remaining size drops by at most `cmax`,
`F_h - cmax ≤ F_{h+1}` pointwise.
Since `c_h` is measurable with respect to the time-`h` history, the identity
`F_h = c_h + E[F_{h+1} | hist h]` always bounds the drop of `F` by `cmax` *in
conditional expectation*; the slow-decrement property demands the same bound
in every individual branch. -/
def ChunkSystemB.SlowDecrement
(C : ChunkSystemB X s t cLo cHi total price mLo) (cmax : ℝ) : Prop :=
∀ (h : ℕ) (ω : C.Ω), C.condRemaining h ω - cmax ≤ C.condRemaining (h + 1) ω
/-- The output of Claim 13 with the slow-decrement property added: the
subchunk system on the next level whose conditional expected remaining size
never drops, in any branch, by more than the maximal subchunk size
`3 * 3 ^ w / 2`. -/
def BCRInductiveSubchunksStable (α : ℝ) (β : ℕ) (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)
/-- At time `0` with trivial initial information the conditional expected remaining size
is exactly the expected total size of the system. -/
theorem ChunkSystemB.condRemaining_zero
(C : ChunkSystemB X s t cLo cHi total price mLo)
(h0 : ∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂) (ω : C.Ω) :
C.condRemaining 0 ω = ∑ ω', C.P ω' * ∑ j, C.size ω' j := by
have hatom : C.atom 0 ω = Finset.univ :=
Finset.filter_true_of_mem fun ω' _ => h0 ω' ω
have hidx : (Finset.univ.filter (fun j : Fin C.m => 0 ≤ (j : ℕ))) = Finset.univ :=
Finset.filter_true_of_mem fun j _ => Nat.zero_le _
simp only [ChunkSystemB.condRemaining, hatom, hidx, C.hPsum, div_one]
/-- The expected total size of a chunk system is a lower bound for the time-`0`
conditional expected remaining size. -/
theorem ChunkSystemB.total_le_condRemaining_zero
(C : ChunkSystemB X s t cLo cHi total price mLo)
(h0 : ∀ ω₁ ω₂ : C.Ω, C.hist 0 ω₁ = C.hist 0 ω₂) (ω : C.Ω) :
total ≤ C.condRemaining 0 ω := by
rw [C.condRemaining_zero h0 ω]; exact C.htotal
end KServer