Theorems · Theorem · functional analysis

lp.norm_sum_single

∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α],
  0 < p.toReal →
    ∀ (f : (i : α) → E i) (s : Finset α), ‖∑ i ∈ s, lp.single p i (f i)‖ ^ p.toReal = ∑ i ∈ s, ‖f i‖ ^ p.toReal

Defined in

Mathlib.Analysis.Normed.Lp.lpSpace

Cited by

0 results in Mathlib

Foundations

Depth 219 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupDecidableEq