Instantiate normalization with weighted sum and product

Proved

WeightedRootIntegralIdentity.weightedRootInstantiateNormalizedAlgebra

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

algebracomplex-analysisgeometric-meanweighted-root

Substituting the weighted arithmetic sum and weighted geometric product into the normalized algebra theorem gives the concrete weighted-root identity.

Formal statement

import Mathlib
open scoped BigOperators
namespace WeightedRootIntegralIdentity
theorem weightedRootInstantiateNormalizedAlgebra
    (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 WeightedRootIntegralIdentity

Source

Apply the accepted normalization theorem with S equal to the finite weighted sum and P equal to the finite weighted product.

View graph