def CommunicationComplexity.Functions.Equality.equality (n : ℕ) (x y : BoolInput n) : Bool

The equality function on n-bit strings. Returns true iff the two inputs are equal.

Equations

• CommunicationComplexity.Functions.Equality.equality n x y = decide (x = y)

@[reducible, inline]

abbrev CommunicationComplexity.Functions.Equality.HashSpace (n k : ℕ) : Type

The public randomness for the hashing protocol: a uniformly random hash function from n-bit strings into Fin (2 ^ k).

Equations

• CommunicationComplexity.Functions.Equality.HashSpace n k = CommunicationComplexity.Functions.Hash.HashSpace (CommunicationComplexity.BoolInput n) (2 ^ k)

instance CommunicationComplexity.Functions.Equality.hashRangeNeZero (k : ℕ) : NeZero (2 ^ k)

theorem CommunicationComplexity.Functions.Equality.communicationComplexity_le (n : ℕ) : Deterministic.communicationComplexity (equality n) ≤ ↑n + 1

The deterministic communication complexity of equality is at most n + 1: Alice sends her n-bit input, Bob computes equality and sends one bit.

theorem CommunicationComplexity.Functions.Equality.communicationComplexity_zero : Deterministic.communicationComplexity (equality 0) = 0

When n = 0, equality has communication complexity 0: both inputs are the unique empty function, so the output is always true.

theorem CommunicationComplexity.Functions.Equality.le_communicationComplexity (n : ℕ) (hn : 1 ≤ n) : ↑(n + 1) ≤ Deterministic.communicationComplexity (equality n)

The deterministic communication complexity of equality on n-bit strings is at least n + 1 (for n ≥ 1). Any monochromatic rectangle containing (x, x) must be {(x, x)}, so there are at least 2^n + 1 rectangles in any partition, which requires n + 1 bits.

theorem CommunicationComplexity.Functions.Equality.communicationComplexity_eq (n : ℕ) : Deterministic.communicationComplexity (equality n) = ↑(if n = 0 then 0 else n + 1)

The exact deterministic communication complexity of equality on n-bit strings: 0 when n = 0, and n + 1 otherwise.

noncomputable def CommunicationComplexity.Functions.Equality.equalityHashProtocol (n k : ℕ) : PublicCoin.FiniteMessage.Protocol (HashSpace n k) (BoolInput n) (BoolInput n) Bool

The standard public-coin equality protocol from a random hash function: Alice sends h x, Bob compares it with h y, and then sends the comparison bit.

Equations

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

@[simp]

theorem CommunicationComplexity.Functions.Equality.equalityHashProtocol_rrun (n k : ℕ) (x y : BoolInput n) (h : HashSpace n k) : (equalityHashProtocol n k).rrun x y h = decide (h x = h y)

@[simp]

theorem CommunicationComplexity.Functions.Equality.equalityHashProtocol_complexity (n k : ℕ) : Deterministic.FiniteMessage.Protocol.complexity (equalityHashProtocol n k) = k + 1

theorem CommunicationComplexity.Functions.Equality.publicCoin_communicationComplexity_le_of_hε (n k : ℕ) {ε : ℝ} (hε : 1 / 2 ^ k < ε) : PublicCoin.communicationComplexity (equality n) ε ≤ ↑k + 1

Public-coin upper bound for equality: if the hash range has size 2 ^ k and 1 / 2 ^ k < ε, then the equality protocol has communication complexity at most k + 1.

theorem CommunicationComplexity.Functions.Equality.publicCoin_communicationComplexity_le (n : ℕ) {ε : ℝ} (hε : 0 < ε) : PublicCoin.communicationComplexity (equality n) ε ≤ ↑(Nat.clog 2 (⌈ε⁻¹⌉₊ + 1)) + 1

Public-coin upper bound for equality as a direct function of ε.