English
Let f be meromorphic in normal form at x and g analytic with g(x) ≠ 0. Then MeromorphicNFAt (g • f) x ↔ MeromorphicNFAt f x.
Русский
Пусть f мероморфна в нормальной форме в x и g аналитична при этом g(x) ≠ 0. Тогда MeromorphicNFAt (g • f) x эквивалентно MeromorphicNFAt f x.
LaTeX
$$$AnalyticAt\ 𝕜\ g\ x \land g\ x \neq 0 \Rightarrow MeromorphicNFAt\ (g \cdot f)\ x \iff MeromorphicNFAt\ f\ x$$$
Lean4
/-- If `f` is any function and `g` is analytic without zero at `z₀`, then `f` is meromorphic in
normal form at `z₀` iff `g • f` is meromorphic in normal form at `z₀`. -/
theorem meromorphicNFAt_smul_iff_right_of_analyticAt (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) :
MeromorphicNFAt (g • f) x ↔ MeromorphicNFAt f x
where
mp
hprod :=
by
have : f =ᶠ[𝓝 x] g⁻¹ • g • f :=
by
filter_upwards [h₁g.continuousAt.preimage_mem_nhds (compl_singleton_mem_nhds_iff.mpr h₂g)]
intro y hy
rw [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff] at hy
simp [hy]
rw [meromorphicNFAt_congr this]
exact hprod.smul_analytic (h₁g.inv h₂g) (inv_ne_zero h₂g)
mpr hf := hf.smul_analytic h₁g h₂g
