English
If f is IsRestricted, then r • f is IsRestricted for any r ∈ R.
Русский
Если f ограничено по c, то r • f ограничено по c для любого r ∈ R.
LaTeX
$$$\mathrm{IsRestricted}(c, f) \Rightarrow \mathrm{IsRestricted}(c, r \cdot f)$$$
Lean4
theorem smul {f : PowerSeries R} (hf : IsRestricted c f) (r : R) : IsRestricted c (r • f) := by
if h : r = 0 then (simpa [h] using zero c)
else
simp_rw [isRestricted_iff, norm_mul, norm_pow, Real.norm_eq_abs, abs_norm] at ⊢ hf
intro ε _
obtain ⟨n, hn⟩ := hf (ε / ‖r‖) (by positivity)
refine ⟨n, fun N hN ↦ ?_⟩
calc
_ ≤ ‖r‖ * ‖(coeff N) f‖ * |c| ^ N := mul_le_mul_of_nonneg (norm_mul_le _ _) (by simp) (by simp) (by simp)
_ < ‖r‖ * (ε / ‖r‖) := by rw [mul_assoc]; aesop
_ = ε := mul_div_cancel₀ _ (by aesop)
