Theorems · Theorem · functional analysis

PiLp.norm_eq_sum

∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → Norm (β i)],
  0 < p.toReal → ∀ (f : PiLp p β), ‖f‖ = (∑ i, ‖f.ofLp i‖ ^ p.toReal) ^ (1 / p.toReal)

Defined in

Mathlib.Analysis.Normed.Lp.PiLp

Cited by

8 results in Mathlib

Foundations

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

Assumes

FintypeNorm