Indexing

This file contains one-way and public-coin bounds for the indexing function.

For the distributional lower-bound strategy (uniform input distribution, answer vectors, and Hamming-ball counting), we follow the proof presentation in:

• Tim Roughgarden, Communication Complexity lecture notes, Section 3 (indexing lower bound via distributional complexity / Yao's framework).

def CommunicationComplexity.Functions.Indexing.indexing (n : ℕ+) (x : Fin ↑n → Bool) (i : Fin ↑n) : Bool

The indexing function: Bob outputs Alice's i-th bit.

Equations

• CommunicationComplexity.Functions.Indexing.indexing n x i = x i

def CommunicationComplexity.Functions.Indexing.trivialProtocol (n : ℕ+) : Deterministic.OneWay.Protocol (Fin ↑n → Bool) (Fin ↑n) Bool

The trivial one-way protocol for indexing: Alice sends her full string.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Indexing.oneWayCommunicationComplexity_le (n : ℕ+) : Deterministic.OneWay.communicationComplexity (indexing n) ≤ ↑↑n

One-way upper bound for indexing: Alice can send all n bits.

theorem CommunicationComplexity.Functions.Indexing.communicationComplexity_le (n : ℕ+) : Deterministic.communicationComplexity (indexing n) ≤ ↑(Nat.clog 2 ↑n) + 1

Deterministic upper bound for indexing: Bob can send his index and then Alice can send the output bit.

theorem CommunicationComplexity.Functions.Indexing.le_oneWayCommunicationComplexity (n : ℕ+) : ↑↑n ≤ Deterministic.OneWay.communicationComplexity (indexing n)

One-way lower bound for indexing: any correct deterministic one-way protocol must send at least n bits.

theorem CommunicationComplexity.Functions.Indexing.oneWayCommunicationComplexity_eq (n : ℕ+) : Deterministic.OneWay.communicationComplexity (indexing n) = ↑↑n

instance CommunicationComplexity.Functions.Indexing.indexNeZero (n : ℕ+) : NeZero ↑n

Coercion helper showing (n : ℕ) is nonzero for n : ℕ+.

noncomputable instance CommunicationComplexity.Functions.Indexing.indexMeasureSpace (n : ℕ+) : MeasureTheory.MeasureSpace (Fin ↑n)

Uniform measure-space structure on Fin n.

Equations

• CommunicationComplexity.Functions.Indexing.indexMeasureSpace n = { toMeasurableSpace := Fin.instMeasurableSpace ↑n, volume := ProbabilityTheory.uniformOn Set.univ }

instance CommunicationComplexity.Functions.Indexing.indexIsProbabilityMeasure (n : ℕ+) : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

Uniform measure on Fin n is a probability measure.

noncomputable instance CommunicationComplexity.Functions.Indexing.indexFiniteProbabilitySpace (n : ℕ+) : FiniteProbabilitySpace (Fin ↑n)

Finite probability-space packaging for uniform Fin n.

Equations

• CommunicationComplexity.Functions.Indexing.indexFiniteProbabilitySpace n = CommunicationComplexity.FiniteProbabilitySpace.of (Fin ↑n)

noncomputable instance CommunicationComplexity.Functions.Indexing.boolInputFiniteProbabilitySpace (n : ℕ+) : FiniteProbabilitySpace (BoolInput ↑n)

Finite probability-space packaging for uniform BoolInput n.

Equations

• CommunicationComplexity.Functions.Indexing.boolInputFiniteProbabilitySpace n = id inferInstance

noncomputable def CommunicationComplexity.Functions.Indexing.indexingInputDist (n : ℕ+) : FiniteProbabilitySpace (BoolInput ↑n × Fin ↑n)

Uniform distribution on indexing inputs (x, i), where x and i are chosen independently and uniformly.

Equations

• CommunicationComplexity.Functions.Indexing.indexingInputDist n = CommunicationComplexity.FiniteProbabilitySpace.of (CommunicationComplexity.BoolInput ↑n × Fin ↑n)

theorem CommunicationComplexity.Functions.Indexing.distributionalError_ge_one_eighth_of_bad_half (n : ℕ+) (p : Deterministic.OneWay.Protocol (BoolInput ↑n) (Fin ↑n) Bool) (hbad : 2 ^ (↑n - 1) ≤ {x : BoolInput ↑n | CommunicationComplexity.Functions.Indexing.badInput✝ n p x}.card) : p.distributionalError (indexingInputDist n) (indexing n) ≥ 1 / 8

Core counting step in the indexing distributional argument: if at least half of Alice inputs are bad (in the answer-vector sense), then the deterministic one-way protocol has distributional error at least 1/8 under the uniform input distribution.

Counting lemmas for the distributional indexing lower bound

theorem CommunicationComplexity.Functions.Indexing.deterministicOneWayDistributionalLowerBound_one_ninth (n : ℕ+) (hn300 : 300 ≤ ↑n) (p : Deterministic.OneWay.Protocol (BoolInput ↑n) (Fin ↑n) Bool) : p.cost ≤ ↑n / 10 → p.distributionalError (indexingInputDist n) (indexing n) > 1 / 9

Deterministic distributional lower bound for indexing under the uniform input distribution: any one-way protocol of cost at most n/10 (for n ≥ 300) has distributional error strictly bigger than 1/9.

def CommunicationComplexity.Functions.Indexing.deterministicOneWayDistributionalLowerBound (n : ℕ+) (ε : ℝ) (c : ℕ) : Prop

Distributional one-way lower-bound hypothesis for indexing at error ε and cost budget c.

Equations

• One or more equations did not get rendered due to their size.

theorem CommunicationComplexity.Functions.Indexing.deterministicOneWayDistributionalLowerBound_one_ninth' (n : ℕ+) (hn300 : 300 ≤ ↑n) : deterministicOneWayDistributionalLowerBound n (1 / 9) (↑n / 10)

Packaged form of deterministicOneWayDistributionalLowerBound_one_ninth using the repository's standard distributional-lower-bound predicate.

theorem CommunicationComplexity.Functions.Indexing.publicCoinOneWay_lower_bound_of_distributional (n : ℕ+) {ε : ℝ} {c : ℕ} (h : deterministicOneWayDistributionalLowerBound n ε c) : ↑c < PublicCoin.OneWay.communicationComplexity (indexing n) ε

Setup lemma: any distributional lower bound against the uniform indexing distribution yields a one-way public-coin lower bound via minimax.

theorem CommunicationComplexity.Functions.Indexing.publicCoinOneWay_linear_lower_bound (n : ℕ+) (h : deterministicOneWayDistributionalLowerBound n (1 / 8) (↑n / 10)) : ↑(↑n / 10) < PublicCoin.OneWay.communicationComplexity (indexing n) (1 / 8)

Convenience specialization of publicCoinOneWay_lower_bound_of_distributional to the common constants used in the indexing proof skeleton.

theorem CommunicationComplexity.Functions.Indexing.publicCoinOneWay_linear_lower_bound_one_ninth (n : ℕ+) (hn300 : 300 ≤ ↑n) : ↑(↑n / 10) < PublicCoin.OneWay.communicationComplexity (indexing n) (1 / 9)

Linear public-coin one-way lower bound for indexing at error threshold 1/9 for all sufficiently large input lengths.