Mission bank parametrization and orientation

Proved

WeightedRootIntegralIdentity.missionBankParametrization

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

complex-analysiskeyhole-contourorientation

At each ordered interval, the upper bank contributes the sine-weighted real integral and the oppositely oriented lower bank contributes its negative.

Formal statement

import Mathlib
open scoped BigOperators Interval

theorem WeightedRootIntegralIdentity.missionBankParametrization
    (n : ℕ) (a : ℕ → ℝ) (k : ℕ)
    (U L : ℝ)
    (hU : U = (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)
    (hL : L = -((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)) :
    U + L = 0 := by sorry

View graph