Boolean functions on the hypercube

A Boolean function is a map {0,1}ⁿ → {0,1}, shared across the library as Cslib.BooleanFunction on Cslib.BitString n. This file sets up block flips, which are the moves of sensitivity and block sensitivity, and partial assignments. The complexity measures are built in Measures.lean.

Main definitions

• BitString.flipBlock B x: x with every coordinate of B flipped.
• Block n: a set of coordinates.
• PartialAssignment n: a partial assignment, fixing some coordinates and leaving others free.
• restrict x S: the partial assignment reading off x on the coordinates in S.
• Agrees: An input is consistent with a partial assignment.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Chapter 12 (Decision Trees); the notions defined here underpin Sections 12.2 and 12.5.1.
• H. Buhrman, R. de Wolf, Complexity measures and decision tree complexity: a survey

Flipping blocks of bits

def Cslib.BitString.flipBlock {n : ℕ} (B : Finset (Fin n)) (x : BitString n) : BitString n

x with every coordinate of B flipped.

Equations

• Cslib.BitString.flipBlock B x j = if j ∈ B then !x j else x j

theorem Cslib.BitString.flipBlock_eq_piecewise {n : ℕ} (B : Finset (Fin n)) (x : BitString n) : flipBlock B x = B.piecewise (fun (j : Fin n) => !x j) x

Flipping B splices the negation of x into x on B.

@[simp]

theorem Cslib.BitString.flipBlock_apply_of_mem {n : ℕ} {B : Finset (Fin n)} {x : BitString n} {j : Fin n} (h : j ∈ B) : flipBlock B x j = !x j

@[simp]

theorem Cslib.BitString.flipBlock_apply_of_notMem {n : ℕ} {B : Finset (Fin n)} {x : BitString n} {j : Fin n} (h : j ∉ B) : flipBlock B x j = x j

@[simp]

theorem Cslib.BitString.flipBlock_empty {n : ℕ} (x : BitString n) : flipBlock ∅ x = x

Flipping no coordinates does nothing.

@[simp]

theorem Cslib.BitString.flipBlock_flipBlock {n : ℕ} (B : Finset (Fin n)) (x : BitString n) : flipBlock B (flipBlock B x) = x

Flipping the same block twice does nothing.

theorem Cslib.BitString.flipBlock_involutive {n : ℕ} (B : Finset (Fin n)) : Function.Involutive (flipBlock B)

Flipping a block is an involution.

@[simp]

theorem Cslib.BitString.flipBlock_singleton {n : ℕ} (i : Fin n) (x : BitString n) : flipBlock {i} x = Function.update x i !x i

Flipping the block {i} is flipping the single bit i.

theorem Cslib.BitString.flipBlock_erase {n : ℕ} {B : Finset (Fin n)} {i : Fin n} (hi : i ∈ B) (x : BitString n) : flipBlock (B.erase i) x = Function.update (flipBlock B x) i (x i)

Flipping B \ {i} is flipping B and then restoring bit i ∈ B.

@[reducible, inline]

abbrev Cslib.QueryComplexity.Block (n : ℕ) : Type

A block: a set of coordinates.

Equations

• Cslib.QueryComplexity.Block n = Finset (Fin n)

Partial assignments

@[reducible, inline]

abbrev Cslib.QueryComplexity.PartialAssignment (n : ℕ) : Type

C i = some b fixes coordinate i to b; C i = none leaves it free.

Equations

• Cslib.QueryComplexity.PartialAssignment n = (Fin n → Option Bool)

def Cslib.QueryComplexity.support {n : ℕ} (C : PartialAssignment n) : Finset (Fin n)

The coordinates the partial assignment fixes.

Equations

• Cslib.QueryComplexity.support C = {i : Fin n | (C i).isSome = true}

@[simp]

theorem Cslib.QueryComplexity.mem_support {n : ℕ} {C : PartialAssignment n} {i : Fin n} : i ∈ support C ↔ (C i).isSome = true

A coordinate lies in the support if and only if the partial assignment fixes it.

def Cslib.QueryComplexity.size {n : ℕ} (C : PartialAssignment n) : ℕ

How many coordinates the partial assignment fixes.

Equations

• Cslib.QueryComplexity.size C = (Cslib.QueryComplexity.support C).card

def Cslib.QueryComplexity.Agrees {n : ℕ} (C : PartialAssignment n) (x : BitString n) : Prop

x agrees with C when it matches C on every fixed coordinate.

Equations

• Cslib.QueryComplexity.Agrees C x = ∀ (i : Fin n) (b : Bool), C i = some b → x i = b

@[instance_reducible]

instance Cslib.QueryComplexity.instDecidableAgrees {n : ℕ} (C : PartialAssignment n) (x : BitString n) : Decidable (Agrees C x)

Equations

• Cslib.QueryComplexity.instDecidableAgrees C x = { decide := decide (∀ (k : ℕ) (h : k < n), (fun (i : Fin n) => ∀ (b : Bool), C i = some b → x i = b) ⟨k, h⟩), reflects_decide := ⋯ }

def Cslib.QueryComplexity.ofBitString {n : ℕ} (x : BitString n) : PartialAssignment n

The total assignment reading off every coordinate of x.

Equations

• Cslib.QueryComplexity.ofBitString x i = some (x i)

@[simp]

theorem Cslib.QueryComplexity.agrees_ofBitString_iff {n : ℕ} {x y : BitString n} : Agrees (ofBitString x) y ↔ y = x

A total assignment read off x is agreed with by x alone.

@[simp]

theorem Cslib.QueryComplexity.size_ofBitString {n : ℕ} (x : BitString n) : size (ofBitString x) = n

Reading off the whole input fixes all n coordinates.

def Cslib.QueryComplexity.restrict {n : ℕ} (x : BitString n) (S : Finset (Fin n)) : PartialAssignment n

The partial assignment reading off x on the coordinates only in S.

Equations

• Cslib.QueryComplexity.restrict x S i = if i ∈ S then some (x i) else none

@[simp]

theorem Cslib.QueryComplexity.agrees_restrict_iff {n : ℕ} {x y : BitString n} {S : Finset (Fin n)} : Agrees (restrict x S) y ↔ ∀ i ∈ S, y i = x i

An input agrees with restrict x S if and only if it matches x on S.

@[simp]

theorem Cslib.QueryComplexity.support_restrict {n : ℕ} (x : BitString n) (S : Finset (Fin n)) : support (restrict x S) = S

restrict x S fixes exactly the coordinates in S.

theorem Cslib.QueryComplexity.eq_restrict_support {n : ℕ} {C : PartialAssignment n} {x : BitString n} (h : Agrees C x) : C = restrict x (support C)

A partial assignment consistent with x is x restricted to its support.