Weighted geometric-mean corollary
ProvedWeightedRootIntegralIdentity.weightedRootGeometricMeanCorollaryV2complex-analysisgeometric-meanweighted-root
The weighted-root identity is equivalently solved for the weighted geometric product.
Formal statement
import Mathlib
open scoped BigOperators
theorem WeightedRootIntegralIdentity.weightedRootGeometricMeanCorollaryV2
(n : ℕ) (a w : ℕ → ℝ) (J : ℝ)
(hidentity : J / Real.pi =
(∑ i ∈ Finset.range n, w i * a i) -
(∏ i ∈ Finset.range n, Real.rpow (a i) (w i))) :
(∏ i ∈ Finset.range n, Real.rpow (a i) (w i)) =
(∑ i ∈ Finset.range n, w i * a i) - J / Real.pi := by sorry