Commit 2026-07-04 15:54 f3853dcb

View on Github →

refactor(LSeries/AbstractFuncEq): IsStrongFEPair predicate (#41329) Weak and strong FE-pairs are constructs used in the proof of functional equations for certain L-functions. Mathematically a StrongFEPair is a WeakFEPair with an additional property (but the same data). Having them as separate structures, as at present, creates some annoying duplication. This gets rid of the StrongFEPair structure and replaces it with a predicate IsStrongFEPair stating that a given WeakFEPair is actually strong.

Estimated changes

Modified Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

added theorem IsStrongFEPair.differentiable_Λ

added theorem IsStrongFEPair.hasMellin

added theorem IsStrongFEPair.hf_top

added theorem IsStrongFEPair.hf_zero

added theorem IsStrongFEPair.symm

added theorem IsStrongFEPair.symm_Λ_eq

added theorem IsStrongFEPair.Λ_eq

added structure IsStrongFEPair

deleted theorem StrongFEPair.differentiable_Λ

deleted theorem StrongFEPair.functional_equation

deleted theorem StrongFEPair.hasMellin

deleted theorem StrongFEPair.hf_top'

deleted theorem StrongFEPair.hf_zero'

deleted def StrongFEPair.symm

deleted theorem StrongFEPair.symm_Λ_eq

deleted def StrongFEPair.Λ

deleted theorem StrongFEPair.Λ_eq

deleted structure StrongFEPair

modified theorem WeakFEPair.differentiable_Λ₀

modified theorem WeakFEPair.hf_zero'

modified theorem WeakFEPair.hf_zero

added theorem WeakFEPair.isStrongFEPair_toStrongFEPair

modified def WeakFEPair.toStrongFEPair

modified theorem WeakFEPair.Λ_residue_zero

added theorem isStrongFEPair_symm

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean

modified def HurwitzZeta.hurwitzOddFEPair

added theorem HurwitzZeta.isStrong_hurwitzOddFEPair