Boolean Function Definitions

Core definitions for Boolean functions on the hypercube Fin n → Bool, including sensitivity.

@[reducible, inline]

abbrev Sensitivity.BoolFun (n : ℕ) : Type

A Boolean function on n variables.

Equations

• Sensitivity.BoolFun n = ((Fin n → Bool) → Bool)

def Sensitivity.flipBit {n : ℕ} (x : Fin n → Bool) (i : Fin n) : Fin n → Bool

Flip the i-th bit of an input.

Equations

• Sensitivity.flipBit x i = Function.update x i !x i

@[simp]

theorem Sensitivity.flipBit_apply_same {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipBit x i i = !x i

@[simp]

theorem Sensitivity.flipBit_apply_ne {n : ℕ} (x : Fin n → Bool) (i : Fin n) {j : Fin n} (h : j ≠ i) : flipBit x i j = x j

@[simp]

theorem Sensitivity.flipBit_flipBit_same {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipBit (flipBit x i) i = x

theorem Sensitivity.flipBit_ne_self {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipBit x i ≠ x

theorem Sensitivity.flipBit_injective {n : ℕ} (x : Fin n → Bool) : Function.Injective (flipBit x)

def Sensitivity.BoolFun.sensitiveAt {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) (i : Fin n) : Prop

Whether f is sensitive at input x in coordinate i.

Equations

• f.sensitiveAt x i = (f (Sensitivity.flipBit x i) ≠ f x)

instance Sensitivity.instDecidableSensitiveAt {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) (i : Fin n) : Decidable (f.sensitiveAt x i)

Equations

• Sensitivity.instDecidableSensitiveAt f x i = inferInstanceAs (Decidable (f (Sensitivity.flipBit x i) ≠ f x))

def Sensitivity.BoolFun.localSensitivity {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) : ℕ

The local sensitivity of f at input x: number of sensitive coordinates.

Equations

• f.localSensitivity x = {i : Fin n | f.sensitiveAt x i}.card

noncomputable def Sensitivity.BoolFun.sensitivity {n : ℕ} (f : BoolFun n) : ℕ

The sensitivity of f: maximum local sensitivity over all inputs.

Equations

• f.sensitivity = Finset.univ.sup fun (x : Fin n → Bool) => f.localSensitivity x

theorem Sensitivity.BoolFun.sensitivity_le {n : ℕ} (f : BoolFun n) : f.sensitivity ≤ n

The sensitivity is at most n.

theorem Sensitivity.BoolFun.localSensitivity_le_sensitivity {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) : f.localSensitivity x ≤ f.sensitivity

The local sensitivity is at most the sensitivity.

def Sensitivity.flipCoords {n : ℕ} (x : Fin n → Bool) (S : Finset (Fin n)) : Fin n → Bool

Flip all bits in a set of coordinates.

Equations

• Sensitivity.flipCoords x S j = if j ∈ S then !x j else x j