English
For non-infinite p, the norm of a constant function into β equals a real multiple of the base norm.
Русский
Для непредельного p норма константной функции в β равна вещественному множителю от нормы β.
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.nnnorm_toLp_const` for a version which exchanges the hypothesis `Nonempty ι`.
for `p ≠ ∞`. -/
theorem nnnorm_toLp_const' {β} [SeminormedAddCommGroup β] [Nonempty ι] (b : β) :
‖toLp p (Function.const ι b)‖₊ = (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖₊ :=
by
rcases em <| p = ∞ with (rfl | hp)
·
simp only [toLp_apply, ENNReal.div_top, ENNReal.toReal_zero, NNReal.rpow_zero, one_mul, nnnorm_eq_ciSup,
Function.const_apply, ciSup_const]
· exact nnnorm_toLp_const hp b
