Theorems · Theorem · functional analysis

WithLp.prod_nnnorm_eq_add

∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β],
  p ≠ ⊤ → ∀ (f : WithLp p (α × β)), ‖f‖₊ = (‖f.fst‖₊ ^ p.toReal + ‖f.snd‖₊ ^ p.toReal) ^ (1 / p.toReal)

Defined in

Mathlib.Analysis.Normed.Lp.ProdLp

Cited by

2 results in Mathlib

Foundations

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

Assumes

FactSeminormedAddCommGroupSeminormedAddCommGroup