L^p norms on finite types

The L^p norm of a real function f on a finite type α, for the uniform distribution, is ‖f‖_p = (𝔼_x |f x| ^ p) ^ (1 / p) (Cslib.lpNorm) O'Donnell, Section 1.3. Its p-th power is the p-th absolute moment (Cslib.lpNorm_rpow), and ‖f‖_2 is the square root of the second moment (Cslib.lpNorm_two). See Complexity.Foundations.Analysis.LpNormMeasure for its agreement with Mathlib's MeasureTheory.lpNorm.

The norm is invariant under equivalences (Cslib.lpNorm_equiv), on a product α × β it is the iterated norm (Cslib.lpNorm_prod), and on a subsingleton type it is the absolute value (Cslib.lpNorm_subsingleton).

Main definitions

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

Main results

• Cslib.lpNorm_rpow, Cslib.lpNorm_two, Cslib.lpNorm_two_sq: the p-th power of ‖f‖_p is the p-th absolute moment, and ‖f‖_2 is the root mean square.
• Cslib.lpNorm_equiv, Cslib.lpNorm_prod, Cslib.lpNorm_subsingleton: invariance under equivalence, iterated norm on a product, and value on a subsingleton type.

References

• R. O'Donnell, Analysis of Boolean Functions

noncomputable def Cslib.lpNorm {α : Type u_1} [Fintype α] (p : ℝ) (f : α → ℝ) : ℝ

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

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

The p-th absolute moment is nonnegative.

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

The L^p norm is nonnegative.

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

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

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

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

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

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

Equivalences, products, and subsingletons

theorem Cslib.lpNorm_equiv {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) (p : ℝ) (f : β → ℝ) : lpNorm p (f ∘ ⇑e) = lpNorm p f

An equivalence of finite domains preserves the L^p norm.

theorem Cslib.lpNorm_prod {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : ℝ) (f : α × β → ℝ) : lpNorm p f = lpNorm p fun (a : α) => lpNorm p fun (b : β) => f (a, b)

The L^p norm on a product is the iterated norm: the norm over α of the norms over β.

theorem Cslib.lpNorm_subsingleton {α : Type u_1} [Fintype α] [Subsingleton α] {p : ℝ} (hp : p ≠ 0) (f : α → ℝ) (x : α) : lpNorm p f = |f x|

On a type with at most one element, the L^p norm at a point is the absolute value.