Substitute the accepted derivative and product evaluations

Proved

WeightedRootIntegralIdentity.weightedRootSubstituteAcceptedEvaluations

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

algebracomplex-analysisresidueweighted-root

If the residue balance contains the real parts d.re and p.re, and the accepted evaluations give d.re=−S and p.re=−P, then the balance simplifies to the weighted arithmetic quantity S minus the weighted product P.

Formal statement

import Mathlib
namespace WeightedRootIntegralIdentity
theorem weightedRootSubstituteAcceptedEvaluations
    (J d p : ℂ) (S P : ℝ)
    (hbalance : J = 2 * Real.pi * Complex.I * (-(d.re : ℂ) + (p.re : ℂ)))
    (hd : d.re = -S)
    (hp : p.re = -P) :
    J = 2 * Real.pi * Complex.I * (((S - P : ℝ) : ℂ)) := by sorry
end WeightedRootIntegralIdentity

Source

Rewrite by the two accepted evaluation identities and normalize the resulting complex scalar expression.

View graph