Concrete sine-weighted bank expansion
ProvedWeightedRootIntegralIdentity.concreteSineBankExpansioncomplex-analysissine-weightsweighted-root
The concrete bank expression uses the mission weights sin(pi(k+1)/n)/pi on each ordered interval, exactly matching the displayed sine-weighted sum.
Formal statement
import Mathlib
open scoped BigOperators Interval
theorem WeightedRootIntegralIdentity.concreteSineBankExpansion
(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) :
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 := by sorry