Holomorphicity on the slit annulus (positive inner radius)

Open

WeightedRootIntegralIdentity.weighted_root_keyhole_integrand_differentiableAt_on_slitKeyholeRegion_v2

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

complex-analysisholomorphickeyhole-contourslit-domain

If the inner radius is positive, then 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_v2
    (n : ℕ) (a w : ℕ → ℝ) (r R : ℝ) (z : ℂ)
    (hr : 0 < r) (hz : z ∈ slitKeyholeRegion r R) :
    DifferentiableAt ℂ (weightedRootKeyholeIntegrand n a w) z := by sorry

end WeightedRootIntegralIdentity

Source

Factorwise differentiability of principal powers on the slit plane and nonvanishing of the denominator on a positive-radius annulus.

View graph