Finite weighted-root keyhole contour components (corrected)

import Mathlib
import Definitions.Def_weightedRootKeyholeIntegrand
import Definitions.Def_weightedRootComponentIntegrals
import Definitions.Def_keyholeLineIntegral
open scoped BigOperators Interval

noncomputable def weightedRootFiniteUpperBankIntegral (n : ℕ) (a w : ℕ → ℝ) (a₀ a₁ ε : ℝ) : ℂ :=
  keyholeLineIntegral (weightedRootKeyholeIntegrand n a w) (fun t => ((a₀ + t * (a₁ - a₀) : ℝ) : ℂ) + (ε : ℂ) * Complex.I) 0 1
noncomputable def weightedRootFiniteLowerBankIntegral (n : ℕ) (a w : ℕ → ℝ) (a₀ a₁ ε : ℝ) : ℂ :=
  keyholeLineIntegral (weightedRootKeyholeIntegrand n a w) (fun t => ((a₁ + t * (a₀ - a₁) : ℝ) : ℂ) - (ε : ℂ) * Complex.I) 0 1
noncomputable def weightedRootRightVerticalIntegral (n : ℕ) (a w : ℕ → ℝ) (a₁ ε H : ℝ) : ℂ :=
  keyholeLineIntegral (weightedRootKeyholeIntegrand n a w) (fun t => (a₁ : ℂ) + ((ε + t * (H - ε) : ℝ) : ℂ) * Complex.I) 0 1
noncomputable def weightedRootLeftVerticalIntegral (n : ℕ) (a w : ℕ → ℝ) (a₀ ε H : ℝ) : ℂ :=
  keyholeLineIntegral (weightedRootKeyholeIntegrand n a w) (fun t => (a₀ : ℂ) + ((ε + t * (H - ε) : ℝ) : ℂ) * Complex.I) 0 1
noncomputable def weightedRootFiniteInnerArcIntegral (n : ℕ) (a w : ℕ → ℝ) (r : ℝ) : ℂ := weightedRootInnerArcIntegral n a w r
noncomputable def weightedRootFiniteOuterArcIntegral (n : ℕ) (a w : ℕ → ℝ) (R : ℝ) : ℂ := weightedRootOuterArcIntegral n a w R
noncomputable def weightedRootTruncationEpsilon (m : ℕ) : ℝ := 1 / (m + 1 : ℝ)
noncomputable def weightedRootTruncationHeight (m : ℕ) : ℝ := m + 1