English
The trailing coefficient of the inverse function is the inverse of the trailing coefficient.
Русский
Хвостовой коэффициент обратной функции равен обратному хвостовому коэффициенту.
LaTeX
$$$$ \mathrm{meromorphicTrailingCoeffAt}(f^{-1}, x) = (\mathrm{meromorphicTrailingCoeffAt}(f,x))^{-1}. $$$$
Lean4
/-- The trailing coefficient of the inverse function is the inverse of the trailing coefficient.
-/
theorem meromorphicTrailingCoeffAt_inv {f : 𝕜 → 𝕜} :
meromorphicTrailingCoeffAt f⁻¹ x = (meromorphicTrailingCoeffAt f x)⁻¹ :=
by
by_cases h₁ : MeromorphicAt f x
· by_cases h₂ : meromorphicOrderAt f x = ⊤
· simp_all [meromorphicOrderAt_inv (f := f) (x := x)]
have : f⁻¹ * f =ᶠ[𝓝[≠] x] 1 :=
by
filter_upwards [(meromorphicOrderAt_ne_top_iff_eventually_ne_zero h₁).1 h₂]
simp_all
rw [← mul_eq_one_iff_eq_inv₀ (h₁.meromorphicTrailingCoeffAt_ne_zero h₂), ← h₁.inv.meromorphicTrailingCoeffAt_mul h₁,
meromorphicTrailingCoeffAt_congr_nhdsNE this,
analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := 0)]
· simp
· simp only [zpow_zero, smul_eq_mul, mul_one]
exact eventuallyEq_nhdsWithin_of_eqOn fun _ ↦ congrFun rfl
· simp_all
