English
Let ι be finite and β a family of normed additive groups. For p with p ≠ ∞, the L^p-norm of the constant-ones vector in the product space is equal to the n-th root of the cardinality of ι, times the norm of 1 in β; i.e., the p-norm of (1,1,...,1) equals |ι|^{1/p} · ||1||.
Русский
Пусть ι конечно множество и β—семейство нормируемых абелевых групп. Для p ≠ ∞ нормa L^p константного вектора в произведении равна корню степени p от кардинальности ι, умноженному на норму единицы в β: ||toLp_p(1)|| = |ι|^{1/p} · ||1||.
LaTeX
$$$\|\mathrm{toLp}_p(1_{ι \to β})\| = (|ι|)^{1/p} \cdot \|1_β\|,$$$
Lean4
theorem norm_toLp_one {β} [SeminormedAddCommGroup β] (hp : p ≠ ∞) [One β] :
‖toLp p (1 : ι → β)‖ = (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖(1 : β)‖ :=
(norm_toLp_const hp (1 : β)).trans rfl
