English
The order of the reciprocal is the negation of the order: meromorphicOrderAt(f^{-1}) x = - meromorphicOrderAt f x.
Русский
Порядок обратной функции равен отрицанию исходного порядка: meromorphicOrderAt(f^{-1}) x = - meromorphicOrderAt f x.
LaTeX
$$$\\operatorname{meromorphicOrderAt} (f^{-1}) x = -\\operatorname{meromorphicOrderAt} f x$$$
Lean4
/-- The order of the inverse is the negative of the order. -/
theorem meromorphicOrderAt_inv {f : 𝕜 → 𝕜} : meromorphicOrderAt (f⁻¹) x = -meromorphicOrderAt f x :=
by
by_cases hf : MeromorphicAt f x; swap
· have : ¬MeromorphicAt (f⁻¹) x := by
contrapose! hf
simpa using hf.inv
simp [hf, this]
by_cases h₂f : meromorphicOrderAt f x = ⊤
· rw [h₂f, ← LinearOrderedAddCommGroupWithTop.neg_top, neg_neg]
rw [meromorphicOrderAt_eq_top_iff] at *
filter_upwards [h₂f]
simp
lift meromorphicOrderAt f x to ℤ using h₂f with a ha
apply (meromorphicOrderAt_eq_int_iff hf.inv).2
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_eq_int_iff hf).1 ha.symm
use g⁻¹, h₁g.inv h₂g, inv_eq_zero.not.2 h₂g
rw [eventually_nhdsWithin_iff] at *
filter_upwards [h₃g]
intro _ h₁a h₂a
simp only [Pi.inv_apply, h₁a h₂a, smul_eq_mul, mul_inv_rev, zpow_neg]
ring
