English
For integer exponent n, meromorphicOrderAt(f^n) at x equals n times meromorphicOrderAt f at x.
Русский
Для целочисленного показателя n мероморфный порядок удовлетворяет meromorphicOrderAt(f^n) = n·meromorphicOrderAt f.
LaTeX
$$$\\operatorname{meromorphicOrderAt} (f^n) x = n \\cdot \\operatorname{meromorphicOrderAt} f x$$$
Lean4
/-- The order multiplies by `n` when taking a meromorphic function to its `n`th power. -/
theorem meromorphicOrderAt_zpow {f : 𝕜 → 𝕜} {x : 𝕜} (hf : MeromorphicAt f x) {n : ℤ} :
meromorphicOrderAt (f ^ n) x = n * meromorphicOrderAt f x := by
-- Trivial case: n = 0
by_cases hn : n = 0
· simp only [hn, zpow_zero, WithTop.coe_zero, zero_mul]
rw [← WithTop.coe_zero, meromorphicOrderAt_eq_int_iff]
· exact ⟨1, analyticAt_const, by simp⟩
· apply MeromorphicAt.const
by_cases h : meromorphicOrderAt f x = ⊤
· simp only [h, ne_eq, WithTop.coe_eq_zero, hn, not_false_eq_true, WithTop.mul_top]
rw [meromorphicOrderAt_eq_top_iff] at *
filter_upwards [h]
intro y hy
simp [hy, zero_zpow n hn]
-- General case
obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff hf).1 h
rw [← WithTop.coe_untop₀_of_ne_top h, ← WithTop.coe_mul, meromorphicOrderAt_eq_int_iff (hf.zpow n)]
use g ^ n, h₁g.zpow h₂g
constructor
· simp_all [zpow_eq_zero_iff hn]
· filter_upwards [h₃g]
intro y hy
rw [Pi.pow_apply, hy, smul_eq_mul, mul_zpow]
congr 1
rw [mul_comm, zpow_mul]
