Elementary Properties of Sensitivity

Basic bounds and symmetries for Boolean function sensitivity.

theorem Sensitivity.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 complement equals the local sensitivity.

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

The sensitivity of the complement equals the sensitivity.

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

Local sensitivity at x is at most n.

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

If f is sensitive at x in coordinate i, then flipping i gives a different value.

theorem Sensitivity.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: if f is sensitive at x in direction i, then f is sensitive at (flipBit x i) in direction i.