Memℓp.all

theorem Memℓp.all : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Finite α] (f : (i : α) → E i), Memℓp f p

The theorem `Memℓp.all` states that for any type `α` which is finite, every function `f` from `α` to `E` (where `E` is a normed add commutative group) satisfies the property `Memℓp f p` for any extended nonnegative real number `p`. The property `Memℓp f p` represents a condition on the function `f` which depends on the value of `p`: if `p` is 0, `f` is finitely supported; if `p` is infinity, the range of the norm of `f` is bounded above; if `p` is between 0 and infinity, the series formed by raising the norm of `f` to the power `p` and summing over all `i` is summable.

More concisely: For any finite type `α` and normed add commutative group `E`, every function `f` from `α` to `E` satisfies the condition that the sum of the `p`-th powers of the norms of `f` over all elements in the domain is convergent for any extended nonnegative real number `p`.