Concrete real-axis jump identity

Proved

WeightedRootIntegralIdentity.weightedRootProveJumpIdentity

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

complex-analysisconjugationjump-integralkeyhole-contour

If the upper-bank limit A is the purely imaginary integral of the real-axis imaginary part, then subtracting its conjugate gives twice i times that integral: A−conj(A)=2i∫ Im(F(x))/x dx.

Formal statement

import Mathlib
open scoped Interval
namespace WeightedRootIntegralIdentity
theorem weightedRootProveJumpIdentity
    (F : ℝ → ℂ) (a₀ a₁ : ℝ) (A : ℂ)
    (hA : A = Complex.I *
      (((∫ x in a₀..a₁, (F x).im / x) : ℝ) : ℂ)) :
    A - starRingEnd ℂ A =
      2 * Complex.I * (((∫ x in a₀..a₁, (F x).im / x) : ℝ) : ℂ) := by sorry
end WeightedRootIntegralIdentity

Source

Use the accepted upper/lower boundary identification and conjugacy, followed by the elementary conjugation identity for a purely imaginary complex number.

View graph