English
When the index set is empty, a different normal form arises; otherwise the standard formula holds.
Русский
Если индексный набор пуст, возникает иная форма; иначе используйте стандартную формулу.
LaTeX
$$$\|toLp(p)(\text{const }ι b)\|_+ = (|ι|)^{1/p}\cdot \|b\|_+$$$
Lean4
/-- When `p = ∞`, this lemma does not hold without the additional assumption `Nonempty ι` because
the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
`PiLp.norm_toLp_const'` for a version which exchanges the hypothesis `p ≠ ∞` for
`Nonempty ι`. -/
theorem norm_toLp_const {β} [SeminormedAddCommGroup β] (hp : p ≠ ∞) (b : β) :
‖toLp p (Function.const ι b)‖ = (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖ :=
(congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_const hp b).trans <| by simp
