Instantiate the abstract limit theorem with actual finite components

Proved

WeightedRootIntegralIdentity.weightedRootInstantiateActualFiniteComponents

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

complex-analysiscomponent-integralskeyhole-contourlimit-passage

For the concrete weighted-root upper bank, lower bank, right and left vertical sides, and inner and outer arcs, any finite contour equation together with their accepted limits yields the limiting bank balance.

Formal statement

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

Source

Instantiate the accepted abstract sequence limit theorem with the six weightedRootFiniteContourComponentsV2 definitions.

View graph