Final constant normalization

Proved

WeightedRootIntegralIdentity.missionFinalConstantNormalization

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

complex-analysisnormalizationweighted-root

The limiting contour balance, after collecting the factors of 2, pi, and i, is exactly the sine-weighted integral identity.

Formal statement

import Mathlib
open scoped BigOperators Interval

theorem WeightedRootIntegralIdentity.missionFinalConstantNormalization
    (n : ℕ) (a : ℕ → ℝ) (B : ℝ)
    (hB : B = ∑ k ∈ Finset.range (n - 1),
      (Real.sin (Real.pi * ((k + 1 : ℝ) / n)) / Real.pi) *
        ∫ x in a k..a (k + 1),
          (∏ i ∈ Finset.range n, Real.rpow |x - a i| ((n : ℝ)⁻¹)) / x)
    (hbalance : B = ((1 : ℝ) / n) * (∑ i ∈ Finset.range n, a i)
      - Real.rpow (∏ i ∈ Finset.range n, a i) ((n : ℝ)⁻¹)) :
    (∑ k ∈ Finset.range (n - 1),
      (Real.sin (Real.pi * ((k + 1 : ℝ) / n)) / Real.pi) *
        ∫ x in a k..a (k + 1),
          (∏ i ∈ Finset.range n, Real.rpow |x - a i| ((n : ℝ)⁻¹)) / x)
      = ((1 : ℝ) / n) * (∑ i ∈ Finset.range n, a i)
        - Real.rpow (∏ i ∈ Finset.range n, a i) ((n : ℝ)⁻¹) := by sorry

View graph