@[reducible, inline]

abbrev CommunicationComplexity.BoolInput (n : ℕ) : Type

The type of n-bit Boolean inputs.

Equations

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

def CommunicationComplexity.zeroInput (n : ℕ) : BoolInput n

The all-zero n-bit Boolean input.

Equations

• CommunicationComplexity.zeroInput n x✝ = false

theorem CommunicationComplexity.exists_true_of_ne_zeroInput {n : ℕ} {x : BoolInput n} (hx : x ≠ zeroInput n) : ∃ (i : Fin n), x i = true

A Boolean input is nonzero exactly when some coordinate is true.

def CommunicationComplexity.boolSign (b : Bool) : ℝ

The ±1 sign attached to a Boolean value. We use 1 for false and -1 for true.

Equations

• CommunicationComplexity.boolSign b = if b = true then -1 else 1

@[simp]

theorem CommunicationComplexity.boolSign_xor (a b : Bool) : boolSign (a ^^ b) = boolSign a * boolSign b

boolSign turns xor into multiplication in {±1}.

theorem CommunicationComplexity.boolSign_sum {α : Type u_1} (s : Finset α) (f : α → Bool) : boolSign (s.sum f) = ∏ i ∈ s, boolSign (f i)

The sign of a Boolean sum factors as the product of the signs of its summands.

theorem CommunicationComplexity.boolSign_mul_boolSign_eq_sub_two_indicator (a b : Bool) : boolSign a * boolSign b = 1 - 2 * if a ≠ b then 1 else 0

Two boolSign factors collapse to 1 - 2 * indicator(a ≠ b).

def CommunicationComplexity.flipAt {n : ℕ} (i : Fin n) (x : BoolInput n) : BoolInput n

Flipping one coordinate of a Boolean input.

Equations

• CommunicationComplexity.flipAt i x = Function.update x i !x i

@[simp]

theorem CommunicationComplexity.flipAt_apply_same {n : ℕ} (i : Fin n) (x : BoolInput n) : flipAt i x i = !x i

@[simp]

theorem CommunicationComplexity.flipAt_apply_ne {n : ℕ} {i j : Fin n} (hij : j ≠ i) (x : BoolInput n) : flipAt i x j = x j

@[simp]

theorem CommunicationComplexity.flipAt_flipAt {n : ℕ} (i : Fin n) (x : BoolInput n) : flipAt i (flipAt i x) = x

theorem CommunicationComplexity.flipAt_bijective {n : ℕ} (i : Fin n) : Function.Bijective (flipAt i)