Korten's top-down adversary

A protocol with d messages of at most m bits cannot separate a density rectangle of small rate: by induction on the messages, each message leaves a density rectangle, at the end no coordinate separates it, and the deficits grow as 194 ^ i k and the rates as (32768 · 194 ^ d k) ^ i p (RoundProtocol.not_solves_bounded_density) Korten, Sections 2 to 4. When the starting sets are density limits of each other, the first message needs no mirror step, which saves one round (RoundProtocol.not_solves_bilateral_density).

Main results

• Cslib.Communication.RoundProtocol.not_solves_density: the adversary, for general parameters.
• Cslib.Communication.RoundProtocol.not_solves_bounded_density: with explicit parameters.
• Cslib.Communication.RoundProtocol.not_solves_bilateral_density: from mutual density limits, with one more message.

References

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

theorem Cslib.Communication.RoundProtocol.not_solves_density {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype M] {d : ℕ} (P : KWRoundProtocol ι M d) {X Y : Finset (ι → Bool)} {m : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (k p : ℕ → ℝ) (hstep : ∀ i < d, 1 ≤ k i ∧ 194 * k i ≤ k (i + 1) ∧ 2 * k i + 2 + m ≤ k (i + 1) ∧ 32768 * k i * p i ≤ p (i + 1)) (hcap : ∀ i ≤ d, p i ≤ 1 / 4) (h : DensityRectangle X Y (p 0) (k 0)) : ¬Solves P DiffersAt ↑X ↑Y

Korten's adversary: a protocol with d messages of at most m bits does not separate a density rectangle of rate p 0 and deficit k 0 when the parameters grow fast enough, 1 ≤ k i, k (i + 1) ≥ max (194 k i) (2 k i + 2 + m) and p (i + 1) ≥ 32768 k i p i, and the rates stay at most 1 / 4.

theorem Cslib.Communication.RoundProtocol.not_solves_bounded_density {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype M] {d : ℕ} (P : KWRoundProtocol ι M d) {X Y : Finset (ι → Bool)} {m k p : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hk : 1 ≤ k) (hmk : m + 1 ≤ k) (hbudget : (32768 * 194 ^ d * k) ^ d * p ≤ 1 / 4) (h : DensityRectangle X Y p k) : ¬Solves P DiffersAt ↑X ↑Y

Korten's adversary with explicit parameters: a protocol with d messages of at most m bits does not separate a density rectangle of rate p and deficit k ≥ max 1 (m + 1) when (32768 · 194 ^ d k) ^ d p ≤ 1 / 4.

theorem Cslib.Communication.RoundProtocol.not_solves_bilateral_density {ι : Type u_1} {M : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype M] {d : ℕ} (P : KWRoundProtocol ι M (d + 1)) {X Y : Finset (ι → Bool)} {m p k : ℝ} (hM : ↑(Fintype.card M) ≤ 2 ^ m) (hm : 0 ≤ m) (hk : 1 ≤ k) (hp : 0 < p) (hX : X.Nonempty) (hY : Y.Nonempty) (hdX : BitString.uniformDeficit X ≤ k) (hdY : BitString.uniformDeficit Y ≤ k) (hleft : ∀ x ∈ X, BitString.IsDensityLimit Y p k x) (hright : ∀ y ∈ Y, BitString.IsDensityLimit X p k y) (hbudget : (32768 * 194 ^ d * (m + k)) ^ d * p ≤ 1 / 4) : ¬Solves P DiffersAt ↑X ↑Y

Korten's adversary from mutual limits: if X and Y are nonempty of deficit at most k ≥ 1 and their points are (p, k)-limits of each other for a rate p > 0, then a protocol with d + 1 messages of at most m ≥ 0 bits does not separate them when (32768 · 194 ^ d (m + k)) ^ d p ≤ 1 / 4.