Documentation

Complexity.Computability.Communication.Corruption

The corruption bound #

Let ν be a distribution on the pairs of inputs and z an output. The function f is (α, δ)-corrupted on z under ν when every rectangle is corrupted by inputs on which f is not z: their ν-mass is at least α times the mass of the inputs on which f is z, up to δ (Corrupted) [Raz92]. A protocol answering z on a leaf rectangle errs on its corrupted part. Summing over the leaves labelled z (Protocol.sum_filter_run_le_mul), a protocol sending c bits and erring with probability err on inputs drawn from ν has α (ν(f⁻¹(z)) - err) ≤ err + 2 ^ c δ (Corrupted.mul_sub_distributionalError_le). So when δ is small, protocols with small error need many bits, with public coins too (Corrupted.mul_sub_le_of_ecomplexityFun_le, by Yao's principle). Unlike the discrepancy bound, the corruption bound constrains only the rectangles on which f is mostly z, so it applies to functions such as disjointness that have large monochromatic rectangles of another value, which make their discrepancy large Kushilevitz and Nisan.

Main definitions #

Main results #

References #

source
def Cslib.Communication.Corrupted {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DecidableEq Z] (ν : PMF (X × Y)) (f : X → Y → Z) (z : Z) (α δ : ℝ) :
Prop

The function f is (α, δ)-corrupted on the value z under ν when on every rectangle A × B the ν-mass of the pairs on which f is not z is at least α times the mass of the pairs on which f is z, up to δ: α ν(A × B ∩ f⁻¹(z)) ≤ ν(A × B \ f⁻¹(z)) + δ.

Instances For
    source
    theorem Cslib.Communication.Corrupted.nonneg {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DecidableEq Z] {ν : PMF (X × Y)} {f : X → Y → Z} {z : Z} {α δ : ℝ} (h : Corrupted ν f z α δ) :
    0 ≤ δ

    The slack δ of a corrupted function is nonnegative: the empty rectangle has no mass.

    source
    theorem Cslib.Communication.Corrupted.mul_sub_distributionalError_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DecidableEq Z] {ν : PMF (X × Y)} {f : X → Y → Z} {z : Z} {α δ : ℝ} [Finite X] [Finite Y] (h : Corrupted ν f z α δ) (hα : 0 ≤ α) (p : Protocol X Y Z) :
    α * ((ν.toOuterMeasure {q : X × Y | f q.1 q.2 = z}).toReal - p.distributionalError ν fun (x : X) (y : Y) (b : Z) => f x y = b) ≤ (p.distributionalError ν fun (x : X) (y : Y) (b : Z) => f x y = b) + 2 ^ p.depth * δ

    The corruption bound for deterministic protocols: if f is (α, δ)-corrupted on z under ν, with α ≥ 0, a protocol erring with probability err on inputs drawn from ν has α (ν(f⁻¹(z)) - err) ≤ err + 2 ^ depth δ.

    source
    theorem Cslib.Communication.Corrupted.mul_sub_le_of_distributionalComplexity_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DecidableEq Z] {ν : PMF (X × Y)} {f : X → Y → Z} {z : Z} {α δ : ℝ} [Finite X] [Finite Y] (h : Corrupted ν f z α δ) (hα : 0 ≤ α) {ε : ℝ} {c : ℕ} (hc : Protocol.distributionalComplexity ε (fun (x : X) (y : Y) (b : Z) => f x y = b) ν ≤ ↑c) :
    α * ((ν.toOuterMeasure {q : X × Y | f q.1 q.2 = z}).toReal - ε) ≤ ε + 2 ^ c * δ

    The corruption bound on distributional complexity: if f is (α, δ)-corrupted on z under ν, with α ≥ 0, and some protocol sending at most c bits errs with probability at most ε on inputs drawn from ν, then α (ν(f⁻¹(z)) - ε) ≤ ε + 2 ^ c δ.

    source
    theorem Cslib.Communication.Corrupted.mul_sub_le_of_ecomplexityFun_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [DecidableEq Z] {ν : PMF (X × Y)} {f : X → Y → Z} {z : Z} {α δ : ℝ} [Finite X] [Finite Y] (h : Corrupted ν f z α δ) (hα : 0 ≤ α) {ε : ℝ} {c : ℕ} (hc : PublicCoin.ecomplexityFun ε f ≤ ↑c) :
    α * ((ν.toOuterMeasure {q : X × Y | f q.1 q.2 = z}).toReal - ε) ≤ ε + 2 ^ c * δ

    The corruption bound on public-coin complexity: if f is (α, δ)-corrupted on z under ν, with α ≥ 0, then a public-coin protocol computing f with error ε and sending at most c bits has α (ν(f⁻¹(z)) - ε) ≤ ε + 2 ^ c δ.