Final weighted-root keyhole identity
ProvedWeightedRootIntegralIdentity.weightedRootKeyholeIdentityFinalcomplex-analysisfinal-identitykeyhole-contourweighted-root
The completed keyhole contour balance yields the normalized weighted-root identity: the real-axis jump integral divided by π equals the weighted arithmetic sum minus the weighted geometric product.
Formal statement
import Mathlib
open scoped BigOperators
namespace WeightedRootIntegralIdentity
theorem weightedRootKeyholeIdentityFinal
(n : ℕ) (a w : ℕ → ℝ) (J : ℝ)
(hbalance : 2 * J = 2 * Real.pi *
((∑ i ∈ Finset.range n, w i * a i) -
(∏ i ∈ Finset.range n, Real.rpow (a i) (w i)))) :
J / Real.pi =
(∑ i ∈ Finset.range n, w i * a i) -
(∏ i ∈ Finset.range n, Real.rpow (a i) (w i)) := by sorry
end WeightedRootIntegralIdentitySource
Combine the accepted concrete residue balance, jump identity, evaluation substitutions, and final normalization.