fun_zpow_nonneg — Mathlib

English

If a function f is analytic on s, then for every natural number n the function x ↦ f(x)^n is analytic on s.

Русский

Если функция f аналитична на s, то для любого натурального n функция x ↦ f(x)^n аналитична на s.

LaTeX

$$$\mathrm{AnalyticOn}_{\mathbb{K}}(f,s) \Rightarrow \forall n \in \mathbb{N}, \mathrm{AnalyticOn}_{\mathbb{K}}(x \mapsto f(x)^n, s)$$$

Lean4

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

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