nnnorm_toLp_one — Mathlib

English

For nonempty ι and p ≠ ∞, the nnNorm of the constant function into β equals a real multiple of the base nnNorm.

Русский

При ненулевом ι и p ≠ ∞ nnNorm константы в PiLp равна вещественному множителю от nnNorm базового β.

LaTeX

$$$\|toLp(p)(\text{const }ι b)\|_{nn} = (|ι|)^{1/p}\,\|b\|_{nn}$$$

Lean4

theorem nnnorm_toLp_one {β} [SeminormedAddCommGroup β] (hp : p ≠ ∞) [One β] :
    ‖toLp p (1 : ι → β)‖₊ = (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖(1 : β)‖₊ :=
  (nnnorm_toLp_const hp (1 : β)).trans rfl

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