Commit 2024-05-27 06:08 c10a24df

View on Github →

feat (NumberTheory/LSeries): Hurwitz zeta (#12897) Add the Hurwitz zeta function (defined as the sum of its even and odd parts, which were already defined in previous PR's).

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/LSeries/HurwitzZeta.lean

added theorem LSeriesHasSum_exp

added theorem cosZeta_eq

added theorem differentiableAt_expZeta

added theorem differentiableAt_hurwitzZeta

added theorem differentiableAt_hurwitzZeta_sub_one_div

added theorem differentiable_expZeta_of_ne_zero

added theorem differentiable_hurwitzZeta_sub_hurwitzZeta

added theorem expZeta_one_sub

added theorem hasSum_expZeta_of_one_lt_re

added theorem hasSum_hurwitzZeta_of_one_lt_re

added theorem hurwitzZetaEven_eq

added theorem hurwitzZetaOdd_eq

added theorem hurwitzZeta_one_sub

added theorem hurwitzZeta_residue_one

added theorem sinZeta_eq

added theorem tendsto_hurwitzZeta_sub_one_div_nhds_one

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean