fun_zpow_nonneg — Mathlib

English

If a function f: E → 𝕝 is analytic at z and the exponent n is a nonnegative integer, then the function x ↦ f(x)^n is analytic at z.

Русский

Если функция f: E → 𝕝 аналитична в точке z и показатель степени n неотрицателен, то x ↦ f(x)^n аналитична в z.

LaTeX

$$$\mathrm{AnalyticWithinAt}_{\mathbb{K}}(f,s,z) \land 0 \le n \Rightarrow \mathrm{AnalyticWithinAt}_{\mathbb{K}}(x \mapsto f(x)^n, s, z)$$$

Lean4

/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic if the exponent is
nonnegative. -/
theorem fun_zpow_nonneg {f : E → 𝕝} {z : E} {s : Set E} {n : ℤ} (hf : AnalyticWithinAt 𝕜 f s z) (hn : 0 ≤ n) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z := by simpa [← zpow_natCast, hn] using hf.pow n.toNat

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