English
If f is meromorphic at x, then its reciprocal function f⁻¹ is meromorphic at x.
Русский
Если f мероморфна в x, то её обратная функция f⁻¹ мероморфна в x.
LaTeX
$$$MeromorphicAt f x \\to MeromorphicAt f^{-1} x$$$
Lean4
@[fun_prop]
theorem inv {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) : MeromorphicAt f⁻¹ x :=
by
rcases hf with ⟨m, hf⟩
by_cases h_eq : (fun z ↦ (z - x) ^ m • f z) =ᶠ[𝓝 x] 0
· -- silly case: f locally 0 near x
refine (MeromorphicAt.const 0 x).congr ?_
rw [eventuallyEq_nhdsWithin_iff]
filter_upwards [h_eq] with z hfz hz
rw [Pi.inv_apply, (smul_eq_zero_iff_right <| pow_ne_zero _ (sub_ne_zero.mpr hz)).mp hfz, inv_zero]
· -- interesting case: use local formula for `f`
obtain ⟨n, g, hg_an, hg_ne, hg_eq⟩ := hf.exists_eventuallyEq_pow_smul_nonzero_iff.mpr h_eq
have : AnalyticAt 𝕜 (fun z ↦ (z - x) ^ (m + 1)) x :=
(analyticAt_id.sub analyticAt_const).pow
_
-- use `m + 1` rather than `m` to damp out any silly issues with the value at `z = x`
refine ⟨n + 1, (this.fun_smul <| hg_an.inv hg_ne).congr ?_⟩
filter_upwards [hg_eq, hg_an.continuousAt.eventually_ne hg_ne] with z hfg hg_ne'
rcases eq_or_ne z x with rfl | hz_ne
· simp only [sub_self, pow_succ, mul_zero, zero_smul]
· simp_rw [smul_eq_mul] at hfg ⊢
have aux1 : f z ≠ 0 :=
by
have : (z - x) ^ n * g z ≠ 0 := mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz_ne)) hg_ne'
rw [← hfg, mul_ne_zero_iff] at this
exact this.2
simp [field, pow_succ', mul_assoc, hfg]
