Final weighted-root integral identity
ProvedWeightedRootIntegralIdentity.weightedRootFinalWeightedRootIdentitycomplex-analysisgeometric-meanweighted-root
After inserting the accepted evaluations of the origin derivative and reciprocal product, the normalized contour balance yields the weighted-root integral identity and its finite weighted geometric-mean expression.
Formal statement
import Mathlib
import Theorems.Thm_WeightedRootIntegralIdentity_weightedRootInstantiateNormalizedAlgebra
open scoped BigOperators
theorem WeightedRootIntegralIdentity.weightedRootFinalWeightedRootIdentity
(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
exact WeightedRootIntegralIdentity.weightedRootInstantiateNormalizedAlgebra n a w J hbalance