English
If f is meromorphic at g(x) and g is analytic at x, then f ∘ g is meromorphic at x.
Русский
Если f мероморфна в g(x) и g аналитична в x, то f ∘ g мероморфна в x.
LaTeX
$$$\\text{MeromorphicAt}(f \\circ g) x$$$
Lean4
theorem comp_analyticAt {g : 𝕜 → 𝕜} (hf : MeromorphicAt f (g x)) (hg : AnalyticAt 𝕜 g x) : MeromorphicAt (f ∘ g) x :=
by
obtain ⟨r, hr⟩ := hf
by_cases hg' : analyticOrderAt (g · - g x) x = ⊤
· -- trivial case: `g` is locally constant near `x`
refine .congr (.const (f (g x)) x) ?_
filter_upwards [nhdsWithin_le_nhds <| analyticOrderAt_eq_top.mp hg'] with z hz
grind
· -- interesting case: `g z - g x` looks like `(z - x) ^ n` times a non-vanishing function
obtain ⟨n, hn⟩ := WithTop.ne_top_iff_exists.mp hg'
obtain ⟨h, han, hne, heq⟩ := (hg.fun_sub analyticAt_const).analyticOrderAt_eq_natCast.mp hn.symm
set j := fun z ↦ (z - g x) ^ r • f z
have : AnalyticAt 𝕜 (fun z ↦ (h z)⁻¹ ^ r • j (g z)) x := by fun_prop (disch := assumption)
refine ⟨n * r, this.congr ?_⟩
filter_upwards [heq, han.continuousAt.tendsto.eventually_ne hne] with z hz hzne
simp only [inv_pow, Function.comp_apply, inv_smul_eq_iff₀ (pow_ne_zero r hzne)]
rw [← mul_smul (h z ^ r), mul_comm, pow_mul, ← mul_pow, ← smul_eq_mul, ← hz]
