Connect path integral to four contour component integrals

Proved

WeightedRootIntegralIdentity.weightedRootPathIntegralComponentDecompositionV4

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

complex-analysiscomponent-decompositionkeyhole-contour

If the assembled path integral P agrees with the keyhole boundary integral, then it equals the oriented sum of the upper and lower banks, both vertical sides, and the inner and outer arcs.

Formal statement

import Mathlib
import Definitions.Def_weightedRootFiniteContourComponentsV2
open scoped BigOperators Interval
namespace WeightedRootIntegralIdentity
theorem weightedRootPathIntegralComponentDecompositionV4
    (n : ℕ) (a w : ℕ → ℝ) (a₀ a₁ r R : ℝ) (P : ℂ)
    (hpath : P = weightedRootBoundaryIntegral n a w a₀ a₁ r R)
    (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) :
    P = 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 := by sorry
end WeightedRootIntegralIdentity

Source

by rw [hpath, hdecomp]

View graph