English
If f : α → E has ℓ^p membership, then c • f is again in ℓ^p for any scalar c in the ring 𝕜, with E_i normed spaces and IsBoundedSMul condition.
Русский
Если функция f: α → E имеет принадлежность к ℓ^p, то c • f также принадлежит ℓ^p для любого скаляра c в кольце 𝕜, при условии ограниченного умножения.
LaTeX
$$$$ \mathrm{Mem}_{\ell^p}(f,p) \Rightarrow \mathrm{Mem}_{\ell^p}(c \cdot f,p). $$$$
Lean4
theorem const_smul {f : ∀ i, E i} (hf : Memℓp f p) (c : 𝕜) : Memℓp (c • f) p :=
by
rcases p.trichotomy with (rfl | rfl | hp)
· apply memℓp_zero
refine hf.finite_dsupport.subset fun i => (?_ : ¬c • f i = 0 → ¬f i = 0)
exact not_imp_not.mpr fun hf' => hf'.symm ▸ smul_zero c
· obtain ⟨A, hA⟩ := hf.bddAbove
refine memℓp_infty ⟨‖c‖ * A, ?_⟩
rintro a ⟨i, rfl⟩
dsimp only [Pi.smul_apply]
refine (norm_smul_le _ _).trans ?_
gcongr
exact hA ⟨i, rfl⟩
· apply memℓp_gen
dsimp only [Pi.smul_apply]
have := (hf.summable hp).mul_left (↑(‖c‖₊ ^ p.toReal) : ℝ)
simp_rw [← coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul, NNReal.summable_coe, ← NNReal.mul_rpow] at this ⊢
refine NNReal.summable_of_le ?_ this
intro i
gcongr
apply nnnorm_smul_le
