Commit 2024-05-13 21:00 73946d00

View on Github →

feat(NumberTheory/LSeries): Odd Hurwitz zeta functions (#12779) This PR adds the analytic continuation and functional equation for the odd part of the Hurwitz zeta function.

Estimated changes

added theorem SignType.intCast_cast
added theorem sign_intCast
added theorem LSeriesHasSum_sin
added def completedSinZeta
added theorem completedSinZeta_neg
added theorem continuousOn_oddKernel
added theorem continuousOn_sinKernel
added theorem hasSum_int_oddKernel
added theorem hasSum_int_sinKernel
added theorem hasSum_int_sinZeta
added theorem hasSum_nat_sinKernel
added theorem hasSum_nat_sinZeta
added def hurwitzOddFEPair
added theorem hurwitzZetaOdd_neg
added theorem hurwitzZetaOdd_one_sub
added theorem isBigO_atTop_oddKernel
added theorem isBigO_atTop_sinKernel
added def jacobiTheta₂''
added theorem jacobiTheta₂''_conj
added def oddKernel
added theorem oddKernel_def'
added theorem oddKernel_def
added theorem oddKernel_neg
added theorem oddKernel_undef
added theorem oddKernel_zero
added def sinKernel
added theorem sinKernel_def
added theorem sinKernel_neg
added theorem sinKernel_undef
added theorem sinKernel_zero
added theorem sinZeta_neg
added theorem sinZeta_one_sub