analyticOrderNatAt_pow — Mathlib

English

For analytic f at z0, the natural-order of f^n at z0 equals n times the natural-order of f at z0.

Русский

Для аналитической функции f в z0 натуральный порядок f^n в z0 равен n-кратно натуральному порядку f в z0.

LaTeX

$$$analyticOrderNatAt\,(f^{n})\, z_0 = n \cdot analyticOrderNatAt\, f\, z_0$$$

Lean4

/-- The order multiplies by `n` when taking an analytic function to its `n`th power. -/
theorem analyticOrderNatAt_pow (hf : AnalyticAt 𝕜 f z₀) (n : ℕ) :
    analyticOrderNatAt (f ^ n) z₀ = n • analyticOrderNatAt f z₀ := by simp [analyticOrderNatAt, analyticOrderAt_pow, hf]

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