Commit 2024-04-19 02:04 f3368d8a

View on Github →

feat(NumberTheory/LSeries): even Hurwitz zeta functions (part 1) (#12147) Add the construction of the even part of the Hurwitz zeta function (via FE pairs).

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

added def completedCosZeta

added theorem completedCosZeta_eq

added theorem completedCosZeta_neg

added theorem completedCosZeta_one_sub

added def completedCosZeta₀

added theorem completedCosZeta₀_neg

added theorem completedCosZeta₀_one_sub

added def completedHurwitzZetaEven

added theorem completedHurwitzZetaEven_eq

added theorem completedHurwitzZetaEven_neg

added theorem completedHurwitzZetaEven_one_sub

added def completedHurwitzZetaEven₀

added theorem completedHurwitzZetaEven₀_neg

added theorem completedHurwitzZetaEven₀_one_sub

added theorem continuousOn_cosKernel

added theorem continuousOn_evenKernel

added def cosKernel

added theorem cosKernel_def

added theorem cosKernel_neg

added theorem cosKernel_undef

added def evenKernel

added theorem evenKernel_def

added theorem evenKernel_eq_cosKernel_of_zero

added theorem evenKernel_functional_equation

added theorem evenKernel_neg

added theorem evenKernel_undef

added theorem hasSum_int_cosKernel

added theorem hasSum_int_cosKernel₀

added theorem hasSum_int_evenKernel

added theorem hasSum_int_evenKernel₀

added theorem hasSum_nat_cosKernel₀

added def hurwitzEvenFEPair

added theorem hurwitzEvenFEPair_neg

added theorem hurwitzEvenFEPair_zero_symm

added theorem isBigO_atTop_cosKernel_sub

added theorem isBigO_atTop_evenKernel_sub

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

added theorem HasProd.congr_fun