English
Applying the right congruence behaves coordinatewise as in the singleton case.
Русский
Применение правого конгруента действует по координатам так же, как и в случае с одним компонентом.
LaTeX
$$$\text{LinearIsometryEquiv.piLpCongrRightApply}(p,e,x)_i = e_i(x_i)$$$
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.nnnorm_equiv_symm_const'` for a version which exchanges the hypothesis `p ≠ ∞` for
`Nonempty ι`. -/
theorem nnnorm_toLp_const {β} [SeminormedAddCommGroup β] (hp : p ≠ ∞) (b : β) :
‖toLp p (Function.const ι b)‖₊ = (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖₊ :=
by
rcases p.dichotomy with (h | h)
· exact False.elim (hp h)
· have ne_zero : p.toReal ≠ 0 := (zero_lt_one.trans_le h).ne'
simp_rw [nnnorm_eq_sum hp, toLp_apply, Function.const_apply, Finset.sum_const, Finset.card_univ, nsmul_eq_mul,
NNReal.mul_rpow, ← NNReal.rpow_mul, mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div,
ENNReal.toReal_one]
