Prove2Me

BCR 2023, Theorem 11 — Ω(log⁡2k)\Omega(\log^2 k) lower bound for small set chasing on k+1k+1 points

Open
KServer.mss_randomized_lower_bound

by Gabewhigham · Sep 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

competitive-analysisk-serverlower-boundsmetrical-service-systemsonline-algorithms

RETIRED: this copy was created in the wrong Lean environment (Mathlib 0df444a) by mistake. The live statement is KServer.mss_randomized_lower_bound in the Mathlib c5ea003 environment, where the k-server mission lives; use that one instead.

Preamble
import Mathlib
import Definitions.Def_KServer_model
import Definitions.Def_KServer_evader
Formal statement
namespace KServer

theorem mss_randomized_lower_bound :
    ∃ c : ℝ, 0 < c ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      ∃ m : MetricSpace (Fin (k + 1)),
        ∀ N : ℝ, ∃ (n : ℕ) (p : Fin n → ℝ) (σ : Fin n → List (Set (Fin (k + 1)))),
          (∀ j, 0 ≤ p j) ∧ (∑ j, p j) = 1 ∧
          (∀ j, ∀ S ∈ σ j, S.Nonempty) ∧
          (∀ x₀ : Fin (k + 1),
            N ≤ ∑ j, p j * @evaderOfflineCost (Fin (k + 1)) m x₀ (σ j)) ∧
          (∀ E : @EvaderAlgorithm (Fin (k + 1)) m,
            c * Real.log k ^ 2
                * ∑ j, p j * @evaderOfflineCost (Fin (k + 1)) m
                    (@EvaderAlgorithm.pos (Fin (k + 1)) m E []) (σ j)
              ≤ ∑ j, p j * @EvaderAlgorithm.cost (Fin (k + 1)) m E (σ j)) := by sorry

end KServer
Source
S. Bubeck, C. Coester, Y. Rabani, 'The randomized k-server conjecture is false!', STOC 2023, https://arxiv.org/abs/2211.05753, Section 4, Theorem 11 (existence, for each n, of an n-point metric space with C_rand^MSS(M, n-1) = Omega(log^2 n)), stated in the distributional form of their Definition 2 and combined with their Theorem 3 (Yao's minimax principle); here n = k+1.

View graph