Cauchy boundary balance for the weighted-root keyhole contour
ProvedWeightedRootIntegralIdentity.weighted_root_keyhole_contour_boundary_balancecomplex-analysiscontour-integralkeyhole-contour
The Cauchy keyhole-contour computation equates twice the slit-bank jump integral with twice pi times the sum of the local origin and reciprocal-infinity contributions. This is the central contour calculation underlying the normalized keyhole identity.
Preamble
import Mathlib open scoped BigOperators Interval
Formal statement
namespace WeightedRootIntegralIdentity
theorem weighted_root_keyhole_contour_boundary_balance
(n : ℕ) (hn : 2 ≤ n) (a w : ℕ → ℝ)
(hpos : ∀ i < n, 0 < a i)
(hmono : ∀ i < n - 1, a i ≤ a (i + 1))
(hwpos : ∀ i < n, 0 < w i)
(hwsum : (∑ i ∈ Finset.range n, w i) = 1) :
2 * (∫ x in a 0..a (n - 1),
(∏ i ∈ Finset.range n,
((x : ℂ) - (a i : ℂ)) ^ (w i : ℂ)).im / x) =
2 * Real.pi *
(-(deriv
(fun u : ℂ =>
∏ i ∈ Finset.range n, (1 - (a i : ℂ) * u) ^ (w i : ℂ)) 0).re +
(∏ i ∈ Finset.range n,
(((0 : ℂ) - (a i : ℂ)) ^ (w i : ℂ))).re) := by sorry
end WeightedRootIntegralIdentitySource
Keyhole-contour Cauchy theorem and the local expansions at zero and infinity.