`L^p` norms on the Boolean cube #

Specializes Cslib.lpNorm to functions on the Boolean cube ι → Bool O'Donnell, Section 1.3. The norm does not see how the coordinates are named (BitString.lpNorm_comp_arrowCongr), 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), and on the cube over no coordinates it is the absolute value (BitString.lpNorm_of_isEmpty).

Main results #

Cslib.BitString.lpNorm_comp_arrowCongr: invariance under coordinate renaming.
Cslib.BitString.lpNorm_sumElim: the norm over a disjoint union of coordinates is the iterated norm.
Cslib.BitString.lpNorm_of_isEmpty: the norm on the empty cube is the absolute value.

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 : ℝ) (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) :

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