Amplification of public-coin protocols

A public-coin protocol computing a Boolean function f with error ε ≤ 1 / 2 can be run 2 r times with independent coins, answering with the strict majority of the outputs (BitString.strictMajorityOn) Kushilevitz and Nisan, Chapter 3. The majority is wrong only if at least r of the runs err (BitString.card_filter_eq_le_half_of_strictMajorityOn_ne), which happens with probability at most (4 ε (1 - ε)) ^ r by the majority tail bound Probability.PMF.iid_card_ge_le, applied to the indicators of the runs that err. The repeated protocol sends at most 2 r times as many bits (PublicCoin.ecomplexity_le_two_mul_mul, PublicCoin.ecomplexityFun_le_two_mul_mul). For error 1 / 3, 2 r runs reduce the error to (8 / 9) ^ r (PublicCoin.ecomplexityFun_le_two_mul_mul_one_third).

The runs are sequenced with Protocol.runAll, which runs a tuple of protocols one after another before combining their outputs. The protocols are drawn independently with Probability.PMF.iid, which unlike the product Probability.PMF.pi applies to the infinite type of protocols.

Main definitions

• Cslib.Communication.PublicCoin.amplify: the strict majority of 2 r independent runs.

Main results

• Cslib.Communication.PublicCoin.Solves.amplify: the error of the majority of 2 r runs.
• Cslib.Communication.PublicCoin.ecomplexity_le_two_mul_mul, Cslib.Communication.PublicCoin.ecomplexityFun_le_two_mul_mul: amplification of public-coin protocols for Boolean functions.
• Cslib.Communication.PublicCoin.ecomplexityFun_le_two_mul_mul_one_third: amplification from error 1 / 3.

References

• E. Kushilevitz and N. Nisan, Communication Complexity

noncomputable def Cslib.Communication.PublicCoin.amplify {X : Type u_1} {Y : Type u_2} (μ : PublicCoin X Y Bool) (r : ℕ) : PublicCoin X Y Bool

The strict majority of 2 r independent runs of μ.

theorem Cslib.Communication.PublicCoin.depth_amplify_le {X : Type u_1} {Y : Type u_2} {μ : PublicCoin X Y Bool} {c : ℕ} (hμ : μ.depth ≤ ↑c) (r : ℕ) : (μ.amplify r).depth ≤ 2 * ↑r * ↑c

The majority of 2 r runs sends at most 2 r times as many bits.

theorem Cslib.Communication.PublicCoin.Solves.amplify {X : Type u_1} {Y : Type u_2} {μ : PublicCoin X Y Bool} {f : X → Y → Bool} {A : Set X} {B : Set Y} {ε : ℝ} (hμ : μ.Solves ε (fun (x : X) (y : Y) (b : Bool) => f x y = b) A B) (hε : ε ≤ 1 / 2) (r : ℕ) : (μ.amplify r).Solves ((4 * ε * (1 - ε)) ^ r) (fun (x : X) (y : Y) (b : Bool) => f x y = b) A B

Amplification: if μ computes f on A × B with error ε ≤ 1 / 2, then the majority of 2 r independent runs computes it with error (4 ε (1 - ε)) ^ r.

theorem Cslib.Communication.PublicCoin.ecomplexity_le_two_mul_mul {X : Type u_1} {Y : Type u_2} {f : X → Y → Bool} {A : Set X} {B : Set Y} {ε : ℝ} (hε : ε ≤ 1 / 2) (r : ℕ) : ecomplexity ((4 * ε * (1 - ε)) ^ r) (fun (x : X) (y : Y) (b : Bool) => f x y = b) A B ≤ 2 * ↑r * ecomplexity ε (fun (x : X) (y : Y) (b : Bool) => f x y = b) A B

Amplification of public-coin protocols: for error ε ≤ 1 / 2, computing a Boolean function on A × B with error (4 ε (1 - ε)) ^ r costs at most 2 r times as much as with error ε.

theorem Cslib.Communication.PublicCoin.ecomplexityFun_le_two_mul_mul {X : Type u_1} {Y : Type u_2} {f : X → Y → Bool} {ε : ℝ} (hε : ε ≤ 1 / 2) (r : ℕ) : ecomplexityFun ((4 * ε * (1 - ε)) ^ r) f ≤ 2 * ↑r * ecomplexityFun ε f

Amplification of public-coin protocols for Boolean functions: for error ε ≤ 1 / 2, computing f with error (4 ε (1 - ε)) ^ r costs at most 2 r times as much as with error ε.

theorem Cslib.Communication.PublicCoin.ecomplexityFun_le_two_mul_mul_one_third {X : Type u_1} {Y : Type u_2} {f : X → Y → Bool} (r : ℕ) : ecomplexityFun ((8 / 9) ^ r) f ≤ 2 * ↑r * ecomplexityFun (1 / 3) f

Amplification from error 1 / 3: 2 r runs reduce the error to (8 / 9) ^ r.