English
For nonempty index set and p ≠ ∞, the nonnegative norm of a constant in PiLp matches the product factor with the base norm.
Русский
При ненулевом наборе индексов и при p ≠ ∞ ноннеgативная норма константы в PiLp совпадает с соответствующим фактором.
LaTeX
$$$\|\text{toLp}(p)(\text{const }ι b)\|_ = (|ι|)^{1/p} \|b\|_+$$$
Lean4
/-- When `IsEmpty ι`, this lemma does not hold without the additional assumption `p ≠ ∞` because
the left-hand side simplifies to `0`, while the right-hand side simplifies to `‖b‖₊`. See
`PiLp.norm_equiv_symm_const` for a version which exchanges the hypothesis `Nonempty ι`.
for `p ≠ ∞`. -/
theorem norm_toLp_const' {β} [SeminormedAddCommGroup β] [Nonempty ι] (b : β) :
‖toLp p (Function.const ι b)‖ = (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖ :=
(congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_toLp_const' b).trans <| by simp
