Finite weighted-root contour equation in component form (corrected)

Proved

WeightedRootIntegralIdentity.weightedRootFiniteContourResidueEquation

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

complex-analysiskeyhole-contourresidue-theoremweighted-root

For the published weighted-root keyhole integrand, if the finite boundary integral decomposes into the two offset banks, two vertical sides, and two circular arcs, and the boundary integral equals the residue contribution, then the sum of those six concrete components equals the residue contribution.

Preamble

import Mathlib
import Definitions.Def_weightedRootFiniteContourComponentsV2
open scoped BigOperators Interval

Formal statement

namespace WeightedRootIntegralIdentity

theorem weightedRootFiniteContourResidueEquation
    (n : ℕ) (a w : ℕ → ℝ) (a₀ a₁ r R : ℝ) (residue : ℂ)
    (hdecomp : weightedRootBoundaryIntegral n a w a₀ a₁ r R =
      weightedRootFiniteUpperBankIntegral n a w a₀ a₁ r +
      weightedRootFiniteLowerBankIntegral n a w a₀ a₁ r +
      weightedRootRightVerticalIntegral n a w a₁ r R +
      weightedRootLeftVerticalIntegral n a w a₀ r R +
      weightedRootFiniteInnerArcIntegral n a w r +
      weightedRootFiniteOuterArcIntegral n a w R)
    (hres : weightedRootBoundaryIntegral n a w a₀ a₁ r R = 2 * Real.pi * Complex.I * residue) :
    weightedRootFiniteUpperBankIntegral n a w a₀ a₁ r +
      weightedRootFiniteLowerBankIntegral n a w a₀ a₁ r +
      weightedRootRightVerticalIntegral n a w a₁ r R +
      weightedRootLeftVerticalIntegral n a w a₀ r R +
      weightedRootFiniteInnerArcIntegral n a w r +
      weightedRootFiniteOuterArcIntegral n a w R = 2 * Real.pi * Complex.I * residue := by sorry

end WeightedRootIntegralIdentity

Source

Substitution of the concrete component decomposition into the finite Cauchy residue equation.

View graph