def CommunicationComplexity.Functions.InnerProduct.boolInputFiniteProbabilitySpace (n : ℕ) : FiniteProbabilitySpace (BoolInput n)

Equations

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

def CommunicationComplexity.Functions.InnerProduct.overlap {n : ℕ} (x y : BoolInput n) : Finset (Fin n)

The coordinates on which both bit-vectors are true.

Equations

• CommunicationComplexity.Functions.InnerProduct.overlap x y = {i : Fin n | (x i && y i) = true}

def CommunicationComplexity.Functions.InnerProduct.innerProduct (n : ℕ) (x y : BoolInput n) : Bool

The mod-2 inner product of two n-bit vectors: it is true exactly when the number of coordinates where both inputs are true is odd.

Equations

• CommunicationComplexity.Functions.InnerProduct.innerProduct n x y = ∑ i : Fin n, (x i && y i)

@[simp]

theorem CommunicationComplexity.Functions.InnerProduct.innerProduct_zero_right {n : ℕ} (x : BoolInput n) : innerProduct n x (zeroInput n) = false

theorem CommunicationComplexity.Functions.InnerProduct.innerProduct_flipAt_eq_xor {n : ℕ} (x y : BoolInput n) (i : Fin n) (hyi : y i = true) : innerProduct n (flipAt i x) y = (innerProduct n x y ^^ true)

Flipping a coordinate where y has a 1 toggles the inner product.

def CommunicationComplexity.Functions.InnerProduct.xorInput {n : ℕ} (y z : BoolInput n) : BoolInput n

Coordinatewise xor of two Boolean inputs.

Equations

• CommunicationComplexity.Functions.InnerProduct.xorInput y z i = (y i ^^ z i)

theorem CommunicationComplexity.Functions.InnerProduct.abs_discrepancy_le_of_isRectangle {n : ℕ} (R : Set (BoolInput n × BoolInput n)) (hR : Rectangle.IsRectangle R) : |discrepancy (innerProduct n) R| ≤ √(1 / 2 ^ n)

Every rectangle has discrepancy at most 2^{-n/2} for the inner product function over the uniform distribution on BoolInput n × BoolInput n.

theorem CommunicationComplexity.Functions.InnerProduct.publicCoin_le_communicationComplexity_of_hbound (k n : ℕ) {ε : ℝ} (hbound : 2 ^ k * √(1 / 2 ^ n) < 1 - 2 * ε) : ↑k < PublicCoin.communicationComplexity (innerProduct n) ε

Public-coin lower bound for inner product from the discrepancy method.