cpow — Mathlib

English

If f and g are analytic on a neighborhood and f avoids nonpositive reals near that neighborhood, then f^g is analytic on the neighborhood.

Русский

Если f и g аналитичны в окрестности и f избегает неотрицательных вещественных значений в этой окрестности, то f^g аналитична в окрестности.

LaTeX

$$$\\text{AnalyticOnNhd}(\\,f^g\, s)$ for some neighborhood s given fa analytic, ga analytic, m: f z ∈ slitPlane for z∈s$$

Lean4

/-- `f z ^ g z` is analytic if `f z` avoids nonpositive reals -/
theorem cpow (fs : AnalyticOnNhd ℂ f s) (gs : AnalyticOnNhd ℂ g s) (m : ∀ z ∈ s, f z ∈ slitPlane) :
    AnalyticOnNhd ℂ (fun z ↦ f z ^ g z) s := fun z n ↦ (fs z n).cpow (gs z n) (m z n)

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