English
If 𝕜 is a normed ring and each component β_i is a normed space, then the scalar action of 𝕜 on PiLp p β is bounded, i.e., IsBoundedSMul 𝕜 (PiLp p β) holds.
Русский
Пусть 𝕜 — нормированное кольцо, и каждый β_i — нормированное пространство; тогда действие скаляра 𝕜 на PiLp p β ограничено, то есть выполняется IsBoundedSMul 𝕜 (PiLp p β).
LaTeX
$$$\mathrm{IsBoundedSMul}_{𝕜}\bigl(\Pi Lp(p,β)\bigr)$$$
Lean4
instance instIsBoundedSMul [SeminormedRing 𝕜] [∀ i, SeminormedAddCommGroup (β i)] [∀ i, Module 𝕜 (β i)]
[∀ i, IsBoundedSMul 𝕜 (β i)] : IsBoundedSMul 𝕜 (PiLp p β) :=
.of_nnnorm_smul_le fun c f => by
rcases p.dichotomy with (rfl | hp)
· rw [← nnnorm_ofLp, ← nnnorm_ofLp, ofLp_smul]
exact nnnorm_smul_le c (ofLp f)
· 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_le_iff hp0, NNReal.mul_rpow, ← NNReal.rpow_mul,
inv_mul_cancel₀ hp0.ne', NNReal.rpow_one, Finset.mul_sum]
simp_rw [← NNReal.mul_rpow, smul_apply]
gcongr
apply nnnorm_smul_le
