English
The trailing coefficient of f^n equals the nth power of the trailing coefficient of f, for integer exponent n.
Русский
Хвостовой коэффициент f^n равен степени n хвостового коэффициента f, для целочисленного показателя n.
LaTeX
$$$$ \mathrm{meromorphicTrailingCoeffAt}(f^n, x) = (\mathrm{meromorphicTrailingCoeffAt}(f, x))^{n}. $$$$
Lean4
/-- The trailing coefficient of the power of a function is the power of the trailing coefficient.
-/
theorem meromorphicTrailingCoeffAt_zpow {n : ℤ} {f : 𝕜 → 𝕜} (h₁ : MeromorphicAt f x) :
meromorphicTrailingCoeffAt (f ^ n) x = (meromorphicTrailingCoeffAt f x) ^ n :=
by
by_cases h₂ : meromorphicOrderAt f x = ⊤
· by_cases h₃ : n = 0
· simp only [h₃, zpow_zero]
apply analyticAt_const.meromorphicTrailingCoeffAt_of_ne_zero (ne_zero_of_eq_one rfl)
· simp_all [meromorphicOrderAt_zpow h₁, zero_zpow n h₃]
· obtain ⟨g, h₁g, h₂g, h₃g⟩ := (meromorphicOrderAt_ne_top_iff h₁).1 h₂
rw [h₁g.meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n := (meromorphicOrderAt f x).untop₀) h₂g h₃g,
(h₁g.zpow h₂g (n := n)).meromorphicTrailingCoeffAt_of_ne_zero_of_eq_nhdsNE (n :=
(meromorphicOrderAt (f ^ n) x).untop₀) (by simp_all [zpow_ne_zero])]
· simp only [Pi.pow_apply]
· filter_upwards [h₃g] with a ha
simp_all [mul_zpow, ← zpow_mul, meromorphicOrderAt_zpow h₁, mul_comm]
