Bennett Local Residue sum eq zero

Proved

D1Bound5.bennettLocalResidue_sum_eq_zero

by tp · Oct 24, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

The sum of the explicitly defined local residues vanishes whenever the numerator has degree at least two below the full denominator degree. No decomposition or cancellation identity is assumed.

Preamble

import Lean.Elab.Tactic.Omega
import Mathlib.Algebra.Polynomial.BigOperators
import Mathlib.Algebra.Polynomial.PartialFractions
import Mathlib.Algebra.Polynomial.RingDivision
import Mathlib.RingTheory.PowerSeries.Binomial
import Mathlib.Tactic.Ring
import Definitions.Def_D1Bound5_BennettLocalResidues_Definitions

Formal statement

section
open Finset

namespace D1Bound5

section Field

variable {F ι : Type*} [Field F] [CharZero F]
variable [Fintype ι] [DecidableEq ι]






















theorem _root_.D1Bound5.bennettLocalResidue_sum_eq_zero (a : ι → F) (ha : Function.Injective a)
    (e : ι → ℕ) (f : Polynomial F)
    (hdeg : f.degree < ((∑ l, (e l + 1)) - 1 : ℕ)) :
    ∑ i, bennettLocalResidue a e f i = 0 := by sorry

end Field

end D1Bound5
end

Source

D1Bound5/BennettLocalResidues.lean, lines 123-137, SHA-256 69884bc84f14bf065cb46a21f71bb9f253dca11c8d085058e033df4ac0004d31. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph