Holomorphicity on the positive weighted-root slit annulus

Open

WeightedRootIntegralIdentity.weighted_root_keyhole_integrand_differentiableAt_on_slitKeyholeRegion_v3

by abcdefg · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

complex-analysisholomorphickeyhole-contourslit-domainweighted-root

For positive inner radius and positive branch points, the weighted-root keyhole integrand is complex differentiable at every point of the annular slit domain.

Preamble

import Mathlib
import Definitions.Def_slitKeyholeRegion
import Definitions.Def_weightedRootKeyholeIntegrand
import Theorems.Thm_WeightedRootIntegralIdentity_weighted_root_differentiableAt_of_shift_mem_slitPlane
open scoped BigOperators Interval

Formal statement

namespace WeightedRootIntegralIdentity

theorem weighted_root_keyhole_integrand_differentiableAt_on_slitKeyholeRegion_v3
    (n : ℕ) (a w : ℕ → ℝ) (r R : ℝ) (z : ℂ)
    (hr : 0 < r) (hpos : ∀ i < n, 0 < a i)
    (hz : z ∈ slitKeyholeRegion r R) :
    DifferentiableAt ℂ (weightedRootKeyholeIntegrand n a w) z := by sorry

end WeightedRootIntegralIdentity

Source

Factorwise principal-power differentiability on the slit plane, positivity of branch points, and nonvanishing of the denominator on the annulus.

View graph