English
If f and g are IsRestricted with parameter c, then f+g is IsRestricted with parameter c.
Русский
Если f и g ограничены по c, то f+g ограничено по c.
LaTeX
$$$\mathrm{IsRestricted}(c, f+g) \leftarrow \mathrm{IsRestricted}(c,f) \land \mathrm{IsRestricted}(c,g)$$$
Lean4
theorem add {f g : PowerSeries R} (hf : IsRestricted c f) (hg : IsRestricted c g) : IsRestricted c (f + g) :=
by
simp only [isRestricted_iff, map_add, norm_mul, norm_pow, Real.norm_eq_abs] at ⊢ hf hg
intro ε hε
obtain ⟨fN, hfN⟩ := hf (ε / 2) (by positivity)
obtain ⟨gN, hgN⟩ := hg (ε / 2) (by positivity)
simp only [abs_norm] at hfN hgN ⊢
refine ⟨max fN gN, fun n hn ↦ ?_⟩
calc
_ ≤ ‖(coeff n) f‖ * |c| ^ n + ‖(coeff n) g‖ * |c| ^ n := by grw [norm_add_le, add_mul]
_ < ε / 2 + ε / 2 := by gcongr <;> grind
_ = ε := by ring
