Density rectangles

The invariant of Korten's top-down adversary Korten, Sections 3 and 4 is a density rectangle X × Y (DensityRectangle): two nonempty sets of deficit at most k, one of which consists of (r, k)-limits of the other for some rate 0 < r ≤ p. The rate may be smaller than p, since density limits need not be monotone in the rate. A density rectangle of rate below 3 / 4 is not separated by any coordinate (DensityRectangle.not_separated), and after a message of m bits from Alice, some message leaves a density rectangle with deficit max (194 k) (2 k + 2 + m) and rate 32768 k p (DensityRectangle.select_left_message): the strong mirror-set lemma (Cslib.BitString.exists_mirror_set) turns the limits around when they face the wrong player.

Main definitions

• Cslib.Communication.DensityRectangle: density rectangles.

Main results

• Cslib.Communication.DensityRectangle.not_separated: no coordinate separates a density rectangle.
• Cslib.Communication.DensityRectangle.select_left_message: a message keeps a density rectangle.

References

• O. Korten, Top-Down Lower Bounds for All Depths

def Cslib.Communication.DensityRectangle {ι : Type u_1} [Fintype ι] [DecidableEq ι] (X Y : Finset (ι → Bool)) (p k : ℝ) : Prop

A density rectangle X × Y of rate p and deficit k: X and Y are nonempty of deficit at most k, and for some rate 0 < r ≤ p, the points of one of them are (r, k)-limits of the other.

theorem Cslib.Communication.DensityRectangle.swap {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X Y : Finset (ι → Bool)} {p k : ℝ} (h : DensityRectangle X Y p k) : DensityRectangle Y X p k

Density rectangles are symmetric.

theorem Cslib.Communication.DensityRectangle.not_separated {ι : Type u_1} [Fintype ι] [DecidableEq ι] {X Y : Finset (ι → Bool)} {p k : ℝ} (h : DensityRectangle X Y p k) (hp : p < 3 / 4) (i : ι) : ¬∀ x ∈ X, ∀ y ∈ Y, x i ≠ y i

No coordinate separates a density rectangle of rate below 3 / 4.

theorem Cslib.Communication.DensityRectangle.select_left_message {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Type u_2} [Fintype M] {X Y : Finset (ι → Bool)} {p p' k k' m : ℝ} (h : DensityRectangle X Y p k) (send : (ι → Bool) → M) (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hk : 1 ≤ k) (hkk : 194 * k ≤ k') (hcost : 2 * k + 2 + m ≤ k') (hscale : 32768 * k * p ≤ p') (hp' : p' ≤ 1 / 4) : ∃ (a : M), ∃ X' ⊆ X, (∀ x ∈ X', send x = a) ∧ DensityRectangle X' Y p' k'

One message keeps a density rectangle: if Alice sends one of at most 2 ^ m messages, some message leaves a density rectangle of rate p' and deficit k', for k ≥ 1, k' ≥ 194 k, k' ≥ 2 k + 2 + m and 32768 k p ≤ p' ≤ 1 / 4.