Concrete bank integral and origin derivative

Proved

WeightedRootIntegralIdentity.bankRealIntegralAndOriginDerivative

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

complex-analysisresidueweighted-root

The bank jump is the displayed sine-weighted real integral, and the origin residue contribution specializes to minus the 1/n weighted arithmetic sum.

Formal statement

import Mathlib
open scoped BigOperators Interval

theorem WeightedRootIntegralIdentity.bankRealIntegralAndOriginDerivative
    (n : ℕ) (a : ℕ → ℝ) (B : ℝ) (d : ℂ)
    (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)
    (hd : d.re = -((n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, a i)) :
    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 ∧
    d.re = -((n : ℝ)⁻¹ * ∑ i ∈ Finset.range n, a i) := by sorry

View graph