Concrete finite-contour equation at the canonical sequence

Proved

WeightedRootIntegralIdentity.weightedRootConcreteFiniteEquationAtSequence

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

complex-analysisfinite-contourkeyhole-contour

For the canonical truncations εₘ=1/(m+1) and Hₘ=m+1, if the actual six finite weighted-root contour components decompose the boundary integral and the boundary integral equals the fixed residue value ρ at every m, then their oriented sum equals ρ at every m.

Formal statement

import Mathlib
import Definitions.Def_weightedRootFiniteContourComponentsV2
open scoped BigOperators Interval
namespace WeightedRootIntegralIdentity
theorem weightedRootConcreteFiniteEquationAtSequence
    (n : ℕ) (a w : ℕ → ℝ) (a₀ a₁ : ℝ) (ρ : ℂ)
    (hdecomp : ∀ m : ℕ,
      weightedRootBoundaryIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ)) (m + 1 : ℝ) =
        weightedRootFiniteUpperBankIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ)) +
        weightedRootFiniteLowerBankIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ)) +
        weightedRootRightVerticalIntegral n a w a₁ (1 / (m + 1 : ℝ)) (m + 1 : ℝ) +
        weightedRootLeftVerticalIntegral n a w a₀ (1 / (m + 1 : ℝ)) (m + 1 : ℝ) +
        weightedRootFiniteInnerArcIntegral n a w (1 / (m + 1 : ℝ)) +
        weightedRootFiniteOuterArcIntegral n a w (m + 1 : ℝ))
    (hres : ∀ m : ℕ,
      weightedRootBoundaryIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ)) (m + 1 : ℝ) = ρ) :
    ∀ m : ℕ,
      weightedRootFiniteUpperBankIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ)) +
      weightedRootFiniteLowerBankIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ)) +
      weightedRootRightVerticalIntegral n a w a₁ (1 / (m + 1 : ℝ)) (m + 1 : ℝ) +
      weightedRootLeftVerticalIntegral n a w a₀ (1 / (m + 1 : ℝ)) (m + 1 : ℝ) +
      weightedRootFiniteInnerArcIntegral n a w (1 / (m + 1 : ℝ)) +
      weightedRootFiniteOuterArcIntegral n a w (m + 1 : ℝ) = ρ := by sorry
end WeightedRootIntegralIdentity

View graph