Concrete finite contour sequence limit

Proved

WeightedRootIntegralIdentity.weightedRootConcreteFiniteSequenceLimit

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

complex-analysisfinite-contourkeyhole-contourlimit-passage

For ε_m=1/(m+1) and H_m=m+1, suppose the six genuine finite weighted-root contour component integrals satisfy the finite contour equation with constant residue ρ and have the accepted bank, vertical-side, and arc limits. Then the limiting bank sum equals ρ.

Formal statement

import Mathlib
import Definitions.Def_weightedRootFiniteContourComponentsV2
open Filter Topology
open scoped BigOperators Interval
namespace WeightedRootIntegralIdentity
theorem weightedRootConcreteFiniteSequenceLimit
    (n : ℕ) (a w : ℕ → ℝ) (a₀ a₁ : ℝ) (U L ρ : ℂ)
    (hu : Tendsto (fun m : ℕ =>
      weightedRootFiniteUpperBankIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ))) atTop (𝓝 U))
    (hl : Tendsto (fun m : ℕ =>
      weightedRootFiniteLowerBankIntegral n a w a₀ a₁ (1 / (m + 1 : ℝ))) atTop (𝓝 L))
    (hvr : Tendsto (fun m : ℕ =>
      weightedRootRightVerticalIntegral n a w a₁ (1 / (m + 1 : ℝ)) (m + 1 : ℝ)) atTop (𝓝 0))
    (hvl : Tendsto (fun m : ℕ =>
      weightedRootLeftVerticalIntegral n a w a₀ (1 / (m + 1 : ℝ)) (m + 1 : ℝ)) atTop (𝓝 0))
    (hi : Tendsto (fun m : ℕ =>
      weightedRootFiniteInnerArcIntegral n a w (1 / (m + 1 : ℝ))) atTop (𝓝 0))
    (ho : Tendsto (fun m : ℕ =>
      weightedRootFiniteOuterArcIntegral n a w (m + 1 : ℝ)) atTop (𝓝 0))
    (hfinite : ∀ 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 : ℝ) = ρ) :
    U + L = ρ := by sorry
end WeightedRootIntegralIdentity

Source

Apply continuity of addition to the six concrete component sequences and uniqueness of limits.

View graph