Boolean Function Definitions

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

Main definitions

• LeanPoolSensitivity.BoolFun — a Boolean function on n variables.
• LeanPoolSensitivity.flipBit — flip the i-th coordinate of an input.
• LeanPoolSensitivity.BoolFun.sensitiveAt — predicate: f changes value when flipping coordinate i at input x.
• LeanPoolSensitivity.BoolFun.localSensitivity — the number of sensitive coordinates of f at a given input.
• LeanPoolSensitivity.BoolFun.sensitivity — the maximum local sensitivity over all inputs.
• LeanPoolSensitivity.flipCoords — flip all bits inside a finite set of coordinates simultaneously.

@[reducible, inline]

abbrev LeanPoolSensitivity.BoolFun (n : ℕ) : Type

A Boolean function on n variables, viewed as a map (Fin n → Bool) → Bool.

Equations

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

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

Flip the i-th bit of an input x : Fin n → Bool, leaving all other coordinates fixed.

Equations

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

@[simp]

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

@[simp]

theorem LeanPoolSensitivity.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 LeanPoolSensitivity.flipBit_flipBit_same {n : ℕ} (x : Fin n → Bool) (i : Fin n) : flipBit (flipBit x i) i = x

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

flipBit x i is never equal to x itself: the i-th coordinate differs.

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

Different coordinates produce different bit flips of x.

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

f is sensitive at input x in coordinate i when flipping bit i changes the value of f.

Equations

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

@[implicit_reducible]

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

Equations

• f.instDecidableSensitiveAt x i = LeanPoolSensitivity.BoolFun.instDecidableSensitiveAt._aux_1 f x i

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

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

Equations

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

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

The sensitivity of f: the maximum of f.localSensitivity x over all inputs x.

Equations

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

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

The sensitivity of any Boolean function on n variables is at most n.

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

The local sensitivity at any specific input is bounded above by the sensitivity of f.

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

Flip all bits whose index lies in the finite set S, leaving the remaining coordinates fixed.

Equations

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