English
There is a NormSMulClass structure on PiLp p β, i.e., an action of a normed ring that respects norms on PiLp p β.
Русский
Существует структура NormSMulClass на PiLp p β, то есть действие нормированного кольца, сохраняющее норму на PiLp p β.
LaTeX
$$$\mathrm{NormSMulClass}_{𝕜}\bigl(PiLp(p,β)\bigr)$$$
Lean4
instance instNormSMulClass [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)] [∀ i, Module 𝕜 (β i)]
[∀ i, NormSMulClass 𝕜 (β i)] : NormSMulClass 𝕜 (PiLp p β) :=
.of_nnnorm_smul fun c f => by
rcases p.dichotomy with (rfl | hp)
· rw [← nnnorm_ofLp, ← nnnorm_ofLp, WithLp.ofLp_smul, nnnorm_smul]
· have hp0 : 0 < p.toReal := zero_lt_one.trans_le hp
have hpt : p ≠ ⊤ := p.toReal_pos_iff_ne_top.mp hp0
rw [nnnorm_eq_sum hpt, nnnorm_eq_sum hpt, one_div, NNReal.rpow_inv_eq_iff hp0.ne', NNReal.mul_rpow, ←
NNReal.rpow_mul, inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, Finset.mul_sum]
simp_rw [← NNReal.mul_rpow, smul_apply, nnnorm_smul]
