@[reducible, inline]

abbrev CommunicationComplexity.BitString (n : ℕ) : Type

n-bit strings, represented as Boolean-valued functions on Fin n.

Equations

• CommunicationComplexity.BitString n = (Fin n → Bool)

def CommunicationComplexity.BitString.signedInner {n : ℕ} (x y : BitString n) : ℤ

The signed inner product of two Boolean strings, viewed through the usual {0,1} to {±1} correspondence. Each agreeing coordinate contributes 1, and each disagreeing coordinate contributes -1.

Equations

• x.signedInner y = ∑ i : Fin n, if x i = y i then 1 else -1

def CommunicationComplexity.BitString.agreementCount {n : ℕ} (x y : BitString n) : ℕ

The number of coordinates on which two bit strings agree.

Equations

• x.agreementCount y = {i : Fin n | x i = y i}.card

theorem CommunicationComplexity.BitString.agreementCount_add_hammingDist_eq_length {n : ℕ} (x y : BitString n) : x.agreementCount y + hammingDist x y = n

The number of agreeing coordinates plus the number of disagreeing coordinates is the total length of the strings.

theorem CommunicationComplexity.BitString.agreementCount_eq_length_sub_hammingDist {n : ℕ} (x y : BitString n) : ↑(x.agreementCount y) = ↑n - ↑(hammingDist x y)

The number of agreeing coordinates is the total length minus the Hamming distance.

theorem CommunicationComplexity.BitString.signedInner_eq_length_sub_twice_hammingDist {n : ℕ} (x y : BitString n) : x.signedInner y = ↑n - 2 * ↑(hammingDist x y)

The signed inner product is the length minus twice the Hamming distance.

theorem CommunicationComplexity.BitString.signedInner_eq_agreementCount_sub_hammingDist {n : ℕ} (x y : BitString n) : x.signedInner y = ↑(x.agreementCount y) - ↑(hammingDist x y)

The signed inner product is the number of agreeing coordinates minus the number of disagreeing coordinates.

theorem CommunicationComplexity.BitString.signedInner_append {m n : ℕ} (x₁ : Fin m → Bool) (x₂ : Fin n → Bool) (y₁ : Fin m → Bool) (y₂ : Fin n → Bool) : signedInner (Fin.append x₁ x₂) (Fin.append y₁ y₂) = signedInner x₁ y₁ + signedInner x₂ y₂

Concatenating two pairs of strings adds their signed inner products.

theorem CommunicationComplexity.BitString.signedInner_comp_cast {m n : ℕ} (h : m = n) (x y : Fin n → Bool) : signedInner (x ∘ Fin.cast h) (y ∘ Fin.cast h) = signedInner x y

Reindexing both inputs along a Fin.cast does not change the signed inner product.

theorem CommunicationComplexity.BitString.signedInner_amplify {a n : ℕ} (x y : BitString n) : signedInner (Fin.repeat a x) (Fin.repeat a y) = ↑a * x.signedInner y

Repeating both inputs a times multiplies the signed inner product by a.