nnnorm_eq_sum — Mathlib

English

For p with 1 ≤ p < ∞ and f in PiLp p β, the NN-norm of f equals the p-th power sum root: ‖f‖₊ = (∑i ‖f_i‖₊^p.toReal)^(1/p.toReal).

Русский

Для p с 1 ≤ p < ∞ и f ∈ PiLp p β имеем равенство: ‖f‖₊ = (∑i ‖f_i‖₊^p)^(1/p).

LaTeX

$$$$ \|f\|_{+} = \left( \sum_{i} \|f_i\|_{+}^{p} \right)^{1/p} $$$$

Lean4

theorem nnnorm_eq_sum {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*} (hp : p ≠ ∞) [∀ i, SeminormedAddCommGroup (β i)]
    (f : PiLp p β) : ‖f‖₊ = (∑ i, ‖f i‖₊ ^ p.toReal) ^ (1 / p.toReal) :=
  by
  ext
  simp [NNReal.coe_sum, norm_eq_sum (p.toReal_pos_iff_ne_top.mpr hp)]

Похожие утверждения