Coin Approximation

Any finite discrete probability space can be approximated by coin flips. This is the key ingredient for showing that protocols over arbitrary finite probability spaces can be simulated by CoinTape protocols.

def CommunicationComplexity.Internal.cdf {m : ℕ} (p : PMF (Fin m)) (n : ℕ) : ENNReal

Equations

• CommunicationComplexity.Internal.cdf p n = ∑ j : Fin m, if ↑j < n then p j else 0

@[simp]

theorem CommunicationComplexity.Internal.cdf_zero {m : ℕ} (p : PMF (Fin m)) : cdf p 0 = 0

theorem CommunicationComplexity.Internal.cdf_succ {m : ℕ} (p : PMF (Fin m)) (n : Fin m) : cdf p (↑n + 1) = cdf p ↑n + p n

theorem CommunicationComplexity.Internal.cdf_one {m : ℕ} (p : PMF (Fin m)) : cdf p m = 1

theorem CommunicationComplexity.Internal.cdf_mono {m : ℕ} (p : PMF (Fin m)) : Monotone (cdf p)

noncomputable def CommunicationComplexity.Internal.invCdf {m : ℕ} [NeZero m] (p : PMF (Fin m)) (x : ENNReal) : Fin m

Equations

• CommunicationComplexity.Internal.invCdf p x = {i : Fin m | CommunicationComplexity.Internal.cdf p ↑i ≤ x}.max' ⋯

theorem CommunicationComplexity.Internal.invCdf_eq_iff {m : ℕ} [NeZero m] (p : PMF (Fin m)) (x : ENNReal) (hx : x < 1) (i : Fin m) : invCdf p x = i ↔ cdf p ↑i ≤ x ∧ x < cdf p (↑i + 1)

noncomputable def CommunicationComplexity.Internal.uniformApprox {m : ℕ} [NeZero m] (p : PMF (Fin m)) (n : ℕ) [NeZero n] : Fin n → Fin m

Equations

• CommunicationComplexity.Internal.uniformApprox p n i = CommunicationComplexity.Internal.invCdf p (↑↑i / ↑n)

theorem CommunicationComplexity.Internal.uniformApprox_approx {m : ℕ} [NeZero m] (p : PMF (Fin m)) (n : ℕ) [NeZero n] (i : Fin m) : ↑{j : Fin n | uniformApprox p n j = i}.card / ↑n ≤ (p i).toReal + 1 / ↑n

theorem CommunicationComplexity.Internal.single_coin_approx {Ω : Type u_1} [FiniteProbabilitySpace Ω] (δ : ℝ) (hδ : 0 < δ) : ∃ (n : ℕ) (φ : CoinTape n → Ω), ∀ (S : Set Ω), MeasureTheory.volume.real (φ ⁻¹' S) ≤ MeasureTheory.volume.real S + δ

For any finite type Ω with a probability measure and any δ > 0, there exist n and φ : CoinTape n → Ω such that for any set S, the pushforward measure exceeds the true measure by at most δ.

noncomputable def CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.toCoinTape {Ω_X : Type u_1} {Ω_Y : Type u_2} [FiniteProbabilitySpace Ω_X] [FiniteProbabilitySpace Ω_Y] {X : Type u_3} {Y : Type u_4} {α : Type u_5} (p : Protocol Ω_X Ω_Y X Y α) (δ : ℝ) (hδ : 0 < δ) : (nX : ℕ) × (nY : ℕ) × Protocol (CoinTape nX) (CoinTape nY) X Y α

Approximate a finite-message protocol over arbitrary finite probability spaces by one over CoinTape. Given δ > 0, produces nX, nY, and a CoinTape-based protocol with the same complexity whose run approximates the original (via inverse CDF construction). This does not depend on any predicate Q.

Equations

• p.toCoinTape δ hδ = ⟨⋯.choose, ⟨⋯.choose, CommunicationComplexity.Deterministic.FiniteMessage.Protocol.comap p (Prod.map ⋯.choose id) (Prod.map ⋯.choose id)⟩⟩

@[simp]

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.toCoinTape_complexity {Ω_X : Type u_1} {Ω_Y : Type u_2} [FiniteProbabilitySpace Ω_X] [FiniteProbabilitySpace Ω_Y] {X : Type u_3} {Y : Type u_4} {α : Type u_5} (p : Protocol Ω_X Ω_Y X Y α) (δ : ℝ) (hδ : 0 < δ) : Deterministic.FiniteMessage.Protocol.complexity (p.toCoinTape δ hδ).snd.snd = Deterministic.FiniteMessage.Protocol.complexity p

theorem CommunicationComplexity.PrivateCoin.FiniteMessage.Protocol.toCoinTape_approxSatisfies {Ω_X : Type u_1} {Ω_Y : Type u_2} [FiniteProbabilitySpace Ω_X] [FiniteProbabilitySpace Ω_Y] {X : Type u_3} {Y : Type u_4} {α : Type u_5} (p : Protocol Ω_X Ω_Y X Y α) (Q : X → Y → α → Prop) (ε δ : ℝ) (hδ : 0 < δ) (hp : p.ApproxSatisfies Q ε) : (p.toCoinTape δ hδ).snd.snd.ApproxSatisfies Q (ε + δ)

The CoinTape approximation of a protocol preserves ApproxSatisfies up to the given slack δ.