Final weighted root algebraic normalization

Proved

WeightedRootIntegralIdentity.weightedRootFinalAlgebraicNormalization

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

algebracomplex-analysisnormalizationweighted-root

Once the contour calculation gives 2J=2π(S−P), where J is the real-axis jump integral, S the weighted arithmetic sum, and P the weighted geometric product, division by the nonzero constant π yields the normalized weighted root identity J/π=S−P.

Formal statement

import Mathlib
namespace WeightedRootIntegralIdentity
theorem weightedRootFinalAlgebraicNormalization
    (J S P : ℝ)
    (hbalance : 2 * J = 2 * Real.pi * (S - P)) :
    J / Real.pi = S - P := by sorry
end WeightedRootIntegralIdentity

Source

Cancel the common factor 2 and divide by π, using positivity of π.

View graph