Discrepancy

This file will contain discrepancy-based lower bounds for public-coin communication complexity.

The intended strategy is to combine distributional lower bounds with rectangle arguments.

noncomputable def CommunicationComplexity.discrepancy {X : Type u_1} {Y : Type u_2} [μ : FiniteProbabilitySpace (X × Y)] (g : X → Y → Bool) (S : Set (X × Y)) : ℝ

The discrepancy of a Boolean function g on a subset S ⊆ X × Y with respect to a distribution μ on X × Y. This is the expectation of the indicator of S times the ±1 sign of g.

Equations

• CommunicationComplexity.discrepancy g S = ∫ (xy : X × Y), (if xy ∈ S then 1 else 0) * CommunicationComplexity.boolSign (g xy.1 xy.2)

theorem CommunicationComplexity.discrepancy_eq_prob_false_sub_prob_true {X : Type u_1} {Y : Type u_2} [μ : FiniteProbabilitySpace (X × Y)] (g : X → Y → Bool) (S : Set (X × Y)) : discrepancy g S = MeasureTheory.volume.real {xy : X × Y | xy ∈ S ∧ g xy.1 xy.2 = false} - MeasureTheory.volume.real {xy : X × Y | xy ∈ S ∧ g xy.1 xy.2 = true}

The discrepancy is the probability mass of the false part of g on S, minus the probability mass of the true part of g on S.

theorem CommunicationComplexity.Deterministic.Protocol.one_sub_two_distributionalError_le_two_pow_mul {X : Type u_1} {Y : Type u_2} [μ : FiniteProbabilitySpace (X × Y)] (g : X → Y → Bool) (γ : ℝ) (p : Protocol X Y Bool) (hdisc : ∀ (R : Set (X × Y)), Rectangle.IsRectangle R → |discrepancy g R| ≤ γ) : 1 - 2 * p.distributionalError μ g ≤ 2 ^ p.complexity * γ

Core discrepancy lower bound: if every rectangle has discrepancy at most γ, then the distributional error of a deterministic protocol is constrained by its complexity.

theorem CommunicationComplexity.Deterministic.Protocol.logb_le_complexity_of_distributionalError {X : Type u_1} {Y : Type u_2} [μ : FiniteProbabilitySpace (X × Y)] (g : X → Y → Bool) (γ : ℝ) (p : Protocol X Y Bool) (hdisc : ∀ (R : Set (X × Y)), Rectangle.IsRectangle R → |discrepancy g R| ≤ γ) (hγ : 0 < γ) (herr : 0 < 1 - 2 * p.distributionalError μ g) : Real.logb 2 ((1 - 2 * p.distributionalError μ g) / γ) ≤ ↑p.complexity

Textbook discrepancy lower bound in logarithmic form.

theorem CommunicationComplexity.PublicCoin.communicationComplexity_lower_bound_of_discrepancy {X : Type u_1} {Y : Type u_2} [μ : FiniteProbabilitySpace (X × Y)] (g : X → Y → Bool) (ε γ : ℝ) (n : ℕ) (hdisc : ∀ (R : Set (X × Y)), Rectangle.IsRectangle R → |discrepancy g R| ≤ γ) (hbound : 2 ^ n * γ < 1 - 2 * ε) : ↑n < communicationComplexity g ε