Holomorphicity of the weighted-root keyhole integrand on the slit annulus

Open

WeightedRootIntegralIdentity.weighted_root_keyhole_integrand_differentiableAt_on_slitKeyholeRegion

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

complex-analysisholomorphickeyhole-contourslit-domain

At every point of the annular slit domain, the weighted-root quotient integrand is complex differentiable. Membership excludes the nonnegative real slit and therefore gives the nonzero-imaginary-part condition needed by the factorwise principal-power differentiability theorem.

Preamble

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

Formal statement

namespace WeightedRootIntegralIdentity

theorem weighted_root_keyhole_integrand_differentiableAt_on_slitKeyholeRegion
    (n : ℕ) (a w : ℕ → ℝ) (r R : ℝ) (z : ℂ)
    (hz : z ∈ slitKeyholeRegion r R) :
    DifferentiableAt ℂ (weightedRootKeyholeIntegrand n a w) z := by sorry

end WeightedRootIntegralIdentity

Source

The previously proved differentiability theorem away from the real axis, combined with the defining slit-domain condition.

View graph