cpow — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{AnalyticOn}(\\,f^g\, s)$ given fa analytic on s, ga analytic on s, and m: f z ∈ slitPlane for z∈s$$

Lean4

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

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