Commit 2024-05-30 10:19 f7322469

View on Github →

feat(NumberTheory/LSeries): special values of Hurwitz zeta (#13347) Formulae for Hurwitz zeta functions at negative integers in terms of Bernoulli polynomials.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/NumberTheory/LSeries/HurwitzZeta.lean

Created Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean

added theorem cosZeta_two_mul_nat'

added theorem cosZeta_two_mul_nat

added theorem hurwitzZetaEven_one_sub_two_mul_nat

added theorem hurwitzZetaOdd_neg_two_mul_nat

added theorem hurwitzZeta_neg_nat

added theorem sinZeta_two_mul_nat_add_one'

added theorem sinZeta_two_mul_nat_add_one