Holomorphicity on the branch-safe weighted-root annulus

Proved

WeightedRootIntegralIdentity.weighted_root_keyhole_integrand_differentiableAt_on_branchSafeRegion

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

branch-cutcomplex-analysisholomorphickeyhole-contour

On the branch-safe annular domain, the weighted-root quotient is complex differentiable at every point.

Preamble

import Mathlib
import Definitions.Def_weightedRootBranchSafeRegion
import Definitions.Def_weightedRootKeyholeIntegrand
import Theorems.Thm_WeightedRootIntegralIdentity_weighted_root_differentiableAt_of_shift_mem_slitPlane
open scoped BigOperators

Formal statement

namespace WeightedRootIntegralIdentity

theorem weighted_root_keyhole_integrand_differentiableAt_on_branchSafeRegion
    (n : ℕ) (a w : ℕ → ℝ) (r R : ℝ) (z : ℂ)
    (hr : 0 < r) (hz : z ∈ weightedRootBranchSafeRegion n a r R) :
    DifferentiableAt ℂ (weightedRootKeyholeIntegrand n a w) z := by sorry

end WeightedRootIntegralIdentity

Source

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

View graph