English
Let f and g be meromorphic at x. Then f + g is meromorphic at x.
Русский
Пусть f и g мероморфны в точке x. Тогда f + g мероморфна в x.
LaTeX
$$$MeromorphicAt f x \\to MeromorphicAt g x \\to MeromorphicAt (f + g) x$$$
Lean4
@[fun_prop]
theorem add {f g : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (hg : MeromorphicAt g x) : MeromorphicAt (f + g) x :=
by
rcases hf with ⟨m, hf⟩
rcases hg with ⟨n, hg⟩
refine ⟨max m n, ?_⟩
have :
(fun z ↦ (z - x) ^ max m n • (f + g) z) = fun z ↦
(z - x) ^ (max m n - m) • ((z - x) ^ m • f z) + (z - x) ^ (max m n - n) • ((z - x) ^ n • g z) :=
by
simp_rw [← mul_smul, ← pow_add, Nat.sub_add_cancel (Nat.le_max_left _ _), Nat.sub_add_cancel (Nat.le_max_right _ _),
Pi.add_apply, smul_add]
rw [this]
exact
(((analyticAt_id.sub analyticAt_const).pow _).smul hf).add (((analyticAt_id.sub analyticAt_const).pow _).smul hg)
