fun_zpow — Mathlib

English

If f is analytic at z and f(z) ≠ 0, then the reciprocal map z ↦ f(z)^{-1} is analytic at z.

Русский

Если f аналитична в z и f(z) ≠ 0, то z ↦ f(z)^{-1} аналитично в z.

LaTeX

$$AnalyticAt 𝕜 f z → Ne (f z) 0 → AnalyticAt 𝕜 (f z)^{-1} z$$

Lean4

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
-/
theorem fun_zpow {f : E → 𝕝} {z : E} {n : ℤ} (h₁f : AnalyticAt 𝕜 f z) (h₂f : f z ≠ 0) :
    AnalyticAt 𝕜 (fun x ↦ f x ^ n) z := by
  by_cases hn : 0 ≤ n
  · exact zpow_nonneg h₁f hn
  · rw [(Int.eq_neg_comm.mp rfl : n = -(-n))]
    conv => arg 2; intro x; rw [zpow_neg]
    exact (h₁f.zpow_nonneg (by linarith)).inv (zpow_ne_zero (-n) h₂f)

Похожие утверждения