L^p norms of derivatives of Boolean functions

The derivative of a Boolean function read as signs takes the values 0 and ±1, so its L^p norm is the p-th root of the influence (BitString.lpNorm_derivative_signVal) O'Donnell, Section 9.6. This is how the Kahn–Kalai–Linial theorem feeds influences into hypercontractivity.

Main results

• Cslib.BitString.lpNorm_derivative_signVal: the L^p norm of the derivative of a Boolean function is the p-th root of the influence.

References

• R. O'Donnell, Analysis of Boolean Functions

theorem Cslib.BitString.abs_derivative_signVal_rpow {ι : Type u_1} [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) (x : ι → Bool) {p : ℝ} (hp : p ≠ 0) : |derivative i (fun (x : ι → Bool) => signVal (f x)) x| ^ p = |derivative i (fun (x : ι → Bool) => signVal (f x)) x|

A power of the absolute value of the derivative of a Boolean function, read as signs, is the absolute value: the derivative takes the values 0 and ±1.

theorem Cslib.BitString.lpNorm_derivative_signVal {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → Bool) (i : ι) {p : ℝ} (hp : p ≠ 0) : lpNorm p (derivative i fun (x : ι → Bool) => signVal (f x)) = (influence i fun (x : ι → Bool) => signVal (f x)) ^ p⁻¹

The L^p norm of the derivative of a Boolean function, read as signs, is the p-th root of the influence.