Theorems · Definition · functional analysis

lp

{α : Type u_3} → (E : α → Type u_5) → [inst : (i : α) → NormedAddCommGroup (E i)] → ENNReal → AddSubgroup (PreLp E)

The (little) ℓᵖ space: The additive subgroup of a type synonym of Π i, E i, which consists of those functions f such that Memℓp f p (i.e., f has finite p-norm). The non-dependent version comes equipped with the notation ℓ^p(ι, E) in the lp namespace. When p takes the values 0, 1 or 2, the notation ℓ⁰(ι, E), ℓ¹(ι, E), ℓ²(ι, E) is also available.

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

157 results in Mathlib

Foundations

Depth 212 from the axioms, rests on 5,028 definitions · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroup