Elementary Properties of Sensitivity

Basic bounds and symmetries for the sensitivity of Boolean functions.

Main results

• LeanPoolSensitivity.BoolFun.localSensitivity_not — taking the negation of a Boolean function preserves local sensitivity.
• LeanPoolSensitivity.BoolFun.sensitivity_not — and likewise sensitivity.
• LeanPoolSensitivity.BoolFun.localSensitivity_le — local sensitivity at any input is at most n.
• LeanPoolSensitivity.BoolFun.sensitiveAt_flipBit — the sensitivity predicate is invariant under flipping the same coordinate at the input.

theorem LeanPoolSensitivity.BoolFun.localSensitivity_not {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) : localSensitivity (fun (y : Fin n → Bool) => !f y) x = f.localSensitivity x

The local sensitivity of the negation of f equals the local sensitivity of f.

theorem LeanPoolSensitivity.BoolFun.sensitivity_not {n : ℕ} (f : BoolFun n) : (sensitivity fun (y : Fin n → Bool) => !f y) = f.sensitivity

The sensitivity of the negation of f equals the sensitivity of f.

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

The local sensitivity of f at any input x is at most n.

theorem LeanPoolSensitivity.BoolFun.sensitiveAt_iff {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) (i : Fin n) : f.sensitiveAt x i ↔ f (flipBit x i) ≠ f x

Unfolding lemma: f is sensitive at x in coordinate i iff flipping that coordinate changes the value of f.

theorem LeanPoolSensitivity.BoolFun.sensitiveAt_flipBit {n : ℕ} (f : BoolFun n) (x : Fin n → Bool) (i : Fin n) : f.sensitiveAt (flipBit x i) i ↔ f.sensitiveAt x i

Sensitivity at x is symmetric in the following sense: f is sensitive at x in direction i iff f is sensitive at flipBit x i in direction i.