L^p norms on the Boolean cube

The L^p norm of a real function f on the cube ι → Bool, for the uniform distribution, is ‖f‖_p = (𝔼_x |f x| ^ p) ^ (1 / p) (BitString.lpNorm) O'Donnell, Section 1.3. Its p-th power is the p-th absolute moment (BitString.lpNorm_rpow), and ‖f‖_2 is the square root of the second moment (BitString.lpNorm_two).

The norm does not see how the coordinates are named (BitString.lpNorm_comp_arrowCongr), and on the cube over a disjoint union ι ⊕ κ it is the norm, over the bits in ι, of the norms over the bits in κ (BitString.lpNorm_sumElim): the p-th moment over the product of two cubes is the iterated p-th moment. On the cube over no coordinates, a single point, it is the absolute value (BitString.lpNorm_of_isEmpty).

Main definitions

• Cslib.BitString.lpNorm: the L^p norm ‖f‖_p of a real function on the cube.

Main results

• Cslib.BitString.lpNorm_rpow, Cslib.BitString.lpNorm_two: the p-th power of ‖f‖_p is the p-th absolute moment, and ‖f‖_2 is the root mean square.
• Cslib.BitString.lpNorm_sumElim: the norm over a disjoint union of coordinates is the iterated norm.

References

• R. O'Donnell, Analysis of Boolean Functions

noncomputable def Cslib.BitString.lpNorm {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f : (ι → Bool) → ℝ) : ℝ

The L^p norm ‖f‖_p = (𝔼_x |f x| ^ p) ^ (1 / p) of a real function on the cube, for the uniform distribution.

theorem Cslib.BitString.expect_abs_rpow_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f : (ι → Bool) → ℝ) : 0 ≤ Finset.univ.expect fun (x : ι → Bool) => |f x| ^ p

The p-th absolute moment is nonnegative.

theorem Cslib.BitString.lpNorm_nonneg {ι : Type u_1} [Fintype ι] [DecidableEq ι] (p : ℝ) (f : (ι → Bool) → ℝ) : 0 ≤ lpNorm p f

The L^p norm is nonnegative.

theorem Cslib.BitString.lpNorm_rpow {ι : Type u_1} [Fintype ι] [DecidableEq ι] {p : ℝ} (hp : p ≠ 0) (f : (ι → Bool) → ℝ) : lpNorm p f ^ p = Finset.univ.expect fun (x : ι → Bool) => |f x| ^ p

The p-th power of ‖f‖_p is the p-th absolute moment.

theorem Cslib.BitString.lpNorm_two {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : lpNorm 2 f = √(Finset.univ.expect fun (x : ι → Bool) => f x ^ 2)

‖f‖_2 is the root mean square of f.

theorem Cslib.BitString.lpNorm_two_sq {ι : Type u_1} [Fintype ι] [DecidableEq ι] (f : (ι → Bool) → ℝ) : lpNorm 2 f ^ 2 = Finset.univ.expect fun (x : ι → Bool) => f x ^ 2

The square of ‖f‖_2 is the second moment of f.

Renaming and splitting the coordinates

theorem Cslib.BitString.lpNorm_comp_arrowCongr {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (p : ℝ) (f : (κ → Bool) → ℝ) : (lpNorm p fun (x : ι → Bool) => f fun (j : κ) => x (e.symm j)) = lpNorm p f

Renaming the coordinates preserves the L^p norm.

theorem Cslib.BitString.lpNorm_sumElim {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {p : ℝ} (hp : p ≠ 0) (f : (ι ⊕ κ → Bool) → ℝ) : lpNorm p f = lpNorm p fun (x₁ : ι → Bool) => lpNorm p fun (x₂ : κ → Bool) => f (Sum.elim x₁ x₂)

The L^p norm over a disjoint union of coordinates is the iterated norm: the norm over the bits in ι of the norms over the bits in κ.

theorem Cslib.BitString.lpNorm_of_isEmpty {ι : Type u_1} [Fintype ι] [DecidableEq ι] [IsEmpty ι] {p : ℝ} (hp : p ≠ 0) (f : (ι → Bool) → ℝ) (x : ι → Bool) : lpNorm p f = |f x|

On the cube over no coordinates, a single point, the L^p norm is the absolute value.