Commit 2024-03-20 16:24 5b192fd1

View on Github →

feat(NumberTheory/LSeries): abstract functional equations (#11176) A general framework for proving analytic continuation & functional equations via Mellin transforms.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LSeries/AbstractFuncEq.lean

added theorem StrongFEPair.differentiable_Λ

added theorem StrongFEPair.functional_equation

added theorem StrongFEPair.hasMellin

added theorem StrongFEPair.hf_top'

added theorem StrongFEPair.hf_zero'

added def StrongFEPair.symm

added theorem StrongFEPair.symm_Λ_eq

added def StrongFEPair.Λ

added theorem StrongFEPair.Λ_eq

added structure StrongFEPair

added theorem WeakFEPair.differentiableAt_Λ

added theorem WeakFEPair.differentiable_Λ₀

added def WeakFEPair.f_modif

added theorem WeakFEPair.f_modif_aux1

added theorem WeakFEPair.f_modif_aux2

added theorem WeakFEPair.functional_equation

added theorem WeakFEPair.functional_equation₀

added def WeakFEPair.g_modif

added theorem WeakFEPair.h_feq'

added theorem WeakFEPair.hasMellin

added theorem WeakFEPair.hf_modif_FE

added theorem WeakFEPair.hf_modif_int

added theorem WeakFEPair.hf_zero'

added theorem WeakFEPair.hf_zero

added def WeakFEPair.symm

added theorem WeakFEPair.symm_Λ₀_eq

added def WeakFEPair.toStrongFEPair

added def WeakFEPair.Λ

added theorem WeakFEPair.Λ_residue_k

added theorem WeakFEPair.Λ_residue_zero

added def WeakFEPair.Λ₀

added theorem WeakFEPair.Λ₀_eq

added structure WeakFEPair