Commit 2024-05-30 12:50 dbaf5581

View on Github →

chore(NumberTheory/LSeries): namespace Hurwitz zeta (#13377) This wraps all the code added so far about Hurwitz zeta functions (& their cousins expZeta, cosZeta, etc) in a namespace HurwitzZeta.

Estimated changes

Modified Mathlib/NumberTheory/LSeries/HurwitzZeta.lean

added theorem HurwitzZeta.LSeriesHasSum_exp

added theorem HurwitzZeta.cosZeta_eq

added theorem HurwitzZeta.differentiableAt_expZeta

added theorem HurwitzZeta.differentiableAt_hurwitzZeta

added theorem HurwitzZeta.differentiableAt_hurwitzZeta_sub_one_div

added theorem HurwitzZeta.differentiable_expZeta_of_ne_zero

added theorem HurwitzZeta.differentiable_hurwitzZeta_sub_hurwitzZeta

added theorem HurwitzZeta.expZeta_one_sub

added theorem HurwitzZeta.hasSum_expZeta_of_one_lt_re

added theorem HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re

added theorem HurwitzZeta.hurwitzZetaEven_eq

added theorem HurwitzZeta.hurwitzZetaOdd_eq

added theorem HurwitzZeta.hurwitzZeta_one_sub

added theorem HurwitzZeta.hurwitzZeta_residue_one

added theorem HurwitzZeta.sinZeta_eq

added theorem HurwitzZeta.tendsto_hurwitzZeta_sub_one_div_nhds_one

deleted theorem LSeriesHasSum_exp

deleted theorem cosZeta_eq

deleted theorem differentiableAt_expZeta

deleted theorem differentiableAt_hurwitzZeta

deleted theorem differentiableAt_hurwitzZeta_sub_one_div

deleted theorem differentiable_expZeta_of_ne_zero

deleted theorem differentiable_hurwitzZeta_sub_hurwitzZeta

deleted theorem expZeta_one_sub

deleted theorem hasSum_expZeta_of_one_lt_re

deleted theorem hasSum_hurwitzZeta_of_one_lt_re

deleted theorem hurwitzZetaEven_eq

deleted theorem hurwitzZetaOdd_eq

deleted theorem hurwitzZeta_one_sub

deleted theorem hurwitzZeta_residue_one

deleted theorem sinZeta_eq

deleted theorem tendsto_hurwitzZeta_sub_one_div_nhds_one

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean

added theorem HurwitzZeta.LSeriesHasSum_cos

added def HurwitzZeta.completedCosZeta

added theorem HurwitzZeta.completedCosZeta_eq

added theorem HurwitzZeta.completedCosZeta_neg

added theorem HurwitzZeta.completedCosZeta_one_sub

added theorem HurwitzZeta.completedCosZeta_residue_zero

added def HurwitzZeta.completedCosZeta₀

added theorem HurwitzZeta.completedCosZeta₀_neg

added theorem HurwitzZeta.completedCosZeta₀_one_sub

added def HurwitzZeta.completedHurwitzZetaEven

added theorem HurwitzZeta.completedHurwitzZetaEven_eq

added theorem HurwitzZeta.completedHurwitzZetaEven_neg

added theorem HurwitzZeta.completedHurwitzZetaEven_one_sub

added theorem HurwitzZeta.completedHurwitzZetaEven_residue_one

added theorem HurwitzZeta.completedHurwitzZetaEven_residue_zero

added def HurwitzZeta.completedHurwitzZetaEven₀

added theorem HurwitzZeta.completedHurwitzZetaEven₀_neg

added theorem HurwitzZeta.completedHurwitzZetaEven₀_one_sub

added theorem HurwitzZeta.continuousOn_cosKernel

added theorem HurwitzZeta.continuousOn_evenKernel

added def HurwitzZeta.cosKernel

added theorem HurwitzZeta.cosKernel_def

added theorem HurwitzZeta.cosKernel_neg

added theorem HurwitzZeta.cosKernel_undef

added theorem HurwitzZeta.cosZeta_apply_zero

added theorem HurwitzZeta.cosZeta_neg

added theorem HurwitzZeta.cosZeta_neg_two_mul_nat_add_one

added theorem HurwitzZeta.cosZeta_one_sub

added theorem HurwitzZeta.differentiableAt_completedCosZeta

added theorem HurwitzZeta.differentiableAt_completedHurwitzZetaEven

added theorem HurwitzZeta.differentiableAt_cosZeta

added theorem HurwitzZeta.differentiableAt_hurwitzZetaEven

added theorem HurwitzZeta.differentiableAt_hurwitzZetaEven_sub_one_div

added theorem HurwitzZeta.differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven

added theorem HurwitzZeta.differentiableAt_update_of_residue

added theorem HurwitzZeta.differentiable_completedCosZeta₀

added theorem HurwitzZeta.differentiable_completedHurwitzZetaEven₀

added theorem HurwitzZeta.differentiable_cosZeta_of_ne_zero

added theorem HurwitzZeta.differentiable_hurwitzZetaEven_sub_hurwitzZetaEven

added def HurwitzZeta.evenKernel

added theorem HurwitzZeta.evenKernel_def

added theorem HurwitzZeta.evenKernel_eq_cosKernel_of_zero

added theorem HurwitzZeta.evenKernel_functional_equation

added theorem HurwitzZeta.evenKernel_neg

added theorem HurwitzZeta.evenKernel_undef

added theorem HurwitzZeta.hasSum_int_completedCosZeta

added theorem HurwitzZeta.hasSum_int_completedHurwitzZetaEven

added theorem HurwitzZeta.hasSum_int_cosKernel

added theorem HurwitzZeta.hasSum_int_cosKernel₀

added theorem HurwitzZeta.hasSum_int_cosZeta

added theorem HurwitzZeta.hasSum_int_evenKernel

added theorem HurwitzZeta.hasSum_int_evenKernel₀

added theorem HurwitzZeta.hasSum_int_hurwitzZetaEven

added theorem HurwitzZeta.hasSum_nat_completedCosZeta

added theorem HurwitzZeta.hasSum_nat_cosKernel₀

added theorem HurwitzZeta.hasSum_nat_cosZeta

added theorem HurwitzZeta.hasSum_nat_hurwitzZetaEven

added theorem HurwitzZeta.hasSum_nat_hurwitzZetaEven_of_mem_Icc

added def HurwitzZeta.hurwitzEvenFEPair

added theorem HurwitzZeta.hurwitzEvenFEPair_neg

added theorem HurwitzZeta.hurwitzEvenFEPair_zero_symm

added theorem HurwitzZeta.hurwitzZetaEven_apply_zero

added theorem HurwitzZeta.hurwitzZetaEven_def_of_ne_or_ne

added theorem HurwitzZeta.hurwitzZetaEven_neg

added theorem HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one

added theorem HurwitzZeta.hurwitzZetaEven_one_sub

added theorem HurwitzZeta.hurwitzZetaEven_residue_one

added theorem HurwitzZeta.isBigO_atTop_cosKernel_sub

added theorem HurwitzZeta.isBigO_atTop_evenKernel_sub

added theorem HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one

deleted theorem LSeriesHasSum_cos

deleted def completedCosZeta

deleted theorem completedCosZeta_eq

deleted theorem completedCosZeta_neg

deleted theorem completedCosZeta_one_sub

deleted theorem completedCosZeta_residue_zero

deleted def completedCosZeta₀

deleted theorem completedCosZeta₀_neg

deleted theorem completedCosZeta₀_one_sub

deleted def completedHurwitzZetaEven

deleted theorem completedHurwitzZetaEven_eq

deleted theorem completedHurwitzZetaEven_neg

deleted theorem completedHurwitzZetaEven_one_sub

deleted theorem completedHurwitzZetaEven_residue_one

deleted theorem completedHurwitzZetaEven_residue_zero

deleted def completedHurwitzZetaEven₀

deleted theorem completedHurwitzZetaEven₀_neg

deleted theorem completedHurwitzZetaEven₀_one_sub

deleted theorem continuousOn_cosKernel

deleted theorem continuousOn_evenKernel

deleted def cosKernel

deleted theorem cosKernel_def

deleted theorem cosKernel_neg

deleted theorem cosKernel_undef

deleted theorem cosZeta_apply_zero

deleted theorem cosZeta_neg

deleted theorem cosZeta_neg_two_mul_nat_add_one

deleted theorem cosZeta_one_sub

deleted theorem differentiableAt_completedCosZeta

deleted theorem differentiableAt_completedHurwitzZetaEven

deleted theorem differentiableAt_cosZeta

deleted theorem differentiableAt_hurwitzZetaEven

deleted theorem differentiableAt_hurwitzZetaEven_sub_one_div

deleted theorem differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven

deleted theorem differentiableAt_update_of_residue

deleted theorem differentiable_completedCosZeta₀

deleted theorem differentiable_completedHurwitzZetaEven₀

deleted theorem differentiable_cosZeta_of_ne_zero

deleted theorem differentiable_hurwitzZetaEven_sub_hurwitzZetaEven

deleted def evenKernel

deleted theorem evenKernel_def

deleted theorem evenKernel_eq_cosKernel_of_zero

deleted theorem evenKernel_functional_equation

deleted theorem evenKernel_neg

deleted theorem evenKernel_undef

deleted theorem hasSum_int_completedCosZeta

deleted theorem hasSum_int_completedHurwitzZetaEven

deleted theorem hasSum_int_cosKernel

deleted theorem hasSum_int_cosKernel₀

deleted theorem hasSum_int_cosZeta

deleted theorem hasSum_int_evenKernel

deleted theorem hasSum_int_evenKernel₀

deleted theorem hasSum_int_hurwitzZetaEven

deleted theorem hasSum_nat_completedCosZeta

deleted theorem hasSum_nat_cosKernel₀

deleted theorem hasSum_nat_cosZeta

deleted theorem hasSum_nat_hurwitzZetaEven

deleted theorem hasSum_nat_hurwitzZetaEven_of_mem_Icc

deleted def hurwitzEvenFEPair

deleted theorem hurwitzEvenFEPair_neg

deleted theorem hurwitzEvenFEPair_zero_symm

deleted theorem hurwitzZetaEven_apply_zero

deleted theorem hurwitzZetaEven_def_of_ne_or_ne

deleted theorem hurwitzZetaEven_neg

deleted theorem hurwitzZetaEven_neg_two_mul_nat_add_one

deleted theorem hurwitzZetaEven_one_sub

deleted theorem hurwitzZetaEven_residue_one

deleted theorem isBigO_atTop_cosKernel_sub

deleted theorem isBigO_atTop_evenKernel_sub

deleted theorem tendsto_hurwitzZetaEven_sub_one_div_nhds_one

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean

added theorem HurwitzZeta.LSeriesHasSum_sin

added def HurwitzZeta.completedHurwitzZetaOdd

added theorem HurwitzZeta.completedHurwitzZetaOdd_neg

added theorem HurwitzZeta.completedHurwitzZetaOdd_one_sub

added def HurwitzZeta.completedSinZeta

added theorem HurwitzZeta.completedSinZeta_neg

added theorem HurwitzZeta.completedSinZeta_one_sub

added theorem HurwitzZeta.continuousOn_oddKernel

added theorem HurwitzZeta.continuousOn_sinKernel

added theorem HurwitzZeta.differentiableAt_sinZeta

added theorem HurwitzZeta.differentiable_completedHurwitzZetaOdd

added theorem HurwitzZeta.differentiable_completedSinZeta

added theorem HurwitzZeta.differentiable_hurwitzZetaOdd

added theorem HurwitzZeta.hasSum_int_completedHurwitzZetaOdd

added theorem HurwitzZeta.hasSum_int_completedSinZeta

added theorem HurwitzZeta.hasSum_int_hurwitzZetaOdd

added theorem HurwitzZeta.hasSum_int_oddKernel

added theorem HurwitzZeta.hasSum_int_sinKernel

added theorem HurwitzZeta.hasSum_int_sinZeta

added theorem HurwitzZeta.hasSum_nat_completedSinZeta

added theorem HurwitzZeta.hasSum_nat_hurwitzZetaOdd

added theorem HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc

added theorem HurwitzZeta.hasSum_nat_sinKernel

added theorem HurwitzZeta.hasSum_nat_sinZeta

added def HurwitzZeta.hurwitzOddFEPair

added theorem HurwitzZeta.hurwitzZetaOdd_neg

added theorem HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat_sub_one

added theorem HurwitzZeta.hurwitzZetaOdd_one_sub

added theorem HurwitzZeta.isBigO_atTop_oddKernel

added theorem HurwitzZeta.isBigO_atTop_sinKernel

added def HurwitzZeta.jacobiTheta₂''

added theorem HurwitzZeta.jacobiTheta₂''_add_left

added theorem HurwitzZeta.jacobiTheta₂''_conj

added theorem HurwitzZeta.jacobiTheta₂''_neg_left

added theorem HurwitzZeta.jacobiTheta₂'_functional_equation'

added def HurwitzZeta.oddKernel

added theorem HurwitzZeta.oddKernel_def'

added theorem HurwitzZeta.oddKernel_def

added theorem HurwitzZeta.oddKernel_functional_equation

added theorem HurwitzZeta.oddKernel_neg

added theorem HurwitzZeta.oddKernel_undef

added theorem HurwitzZeta.oddKernel_zero

added def HurwitzZeta.sinKernel

added theorem HurwitzZeta.sinKernel_def

added theorem HurwitzZeta.sinKernel_neg

added theorem HurwitzZeta.sinKernel_undef

added theorem HurwitzZeta.sinKernel_zero

added theorem HurwitzZeta.sinZeta_neg

added theorem HurwitzZeta.sinZeta_neg_two_mul_nat_sub_one

added theorem HurwitzZeta.sinZeta_one_sub

deleted theorem LSeriesHasSum_sin

deleted def completedHurwitzZetaOdd

deleted theorem completedHurwitzZetaOdd_neg

deleted theorem completedHurwitzZetaOdd_one_sub

deleted def completedSinZeta

deleted theorem completedSinZeta_neg

deleted theorem completedSinZeta_one_sub

deleted theorem continuousOn_oddKernel

deleted theorem continuousOn_sinKernel

deleted theorem differentiableAt_sinZeta

deleted theorem differentiable_completedHurwitzZetaOdd

deleted theorem differentiable_completedSinZeta

deleted theorem differentiable_hurwitzZetaOdd

deleted theorem hasSum_int_completedHurwitzZetaOdd

deleted theorem hasSum_int_completedSinZeta

deleted theorem hasSum_int_hurwitzZetaOdd

deleted theorem hasSum_int_oddKernel

deleted theorem hasSum_int_sinKernel

deleted theorem hasSum_int_sinZeta

deleted theorem hasSum_nat_completedSinZeta

deleted theorem hasSum_nat_hurwitzZetaOdd

deleted theorem hasSum_nat_hurwitzZetaOdd_of_mem_Icc

deleted theorem hasSum_nat_sinKernel

deleted theorem hasSum_nat_sinZeta

deleted def hurwitzOddFEPair

deleted theorem hurwitzZetaOdd_neg

deleted theorem hurwitzZetaOdd_neg_two_mul_nat_sub_one

deleted theorem hurwitzZetaOdd_one_sub

deleted theorem isBigO_atTop_oddKernel

deleted theorem isBigO_atTop_sinKernel

deleted def jacobiTheta₂''

deleted theorem jacobiTheta₂''_add_left

deleted theorem jacobiTheta₂''_conj

deleted theorem jacobiTheta₂''_neg_left

deleted theorem jacobiTheta₂'_functional_equation'

deleted def oddKernel

deleted theorem oddKernel_def'

deleted theorem oddKernel_def

deleted theorem oddKernel_functional_equation

deleted theorem oddKernel_neg

deleted theorem oddKernel_undef

deleted theorem oddKernel_zero

deleted def sinKernel

deleted theorem sinKernel_def

deleted theorem sinKernel_neg

deleted theorem sinKernel_undef

deleted theorem sinKernel_zero

deleted theorem sinZeta_neg

deleted theorem sinZeta_neg_two_mul_nat_sub_one

deleted theorem sinZeta_one_sub

Modified Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean

added theorem HurwitzZeta.cosZeta_two_mul_nat'

added theorem HurwitzZeta.cosZeta_two_mul_nat

added theorem HurwitzZeta.hurwitzZetaEven_one_sub_two_mul_nat

added theorem HurwitzZeta.hurwitzZetaOdd_neg_two_mul_nat

added theorem HurwitzZeta.hurwitzZeta_neg_nat

added theorem HurwitzZeta.sinZeta_two_mul_nat_add_one'

added theorem HurwitzZeta.sinZeta_two_mul_nat_add_one

deleted theorem cosZeta_two_mul_nat'

deleted theorem cosZeta_two_mul_nat

deleted theorem hurwitzZetaEven_one_sub_two_mul_nat

deleted theorem hurwitzZetaOdd_neg_two_mul_nat

deleted theorem hurwitzZeta_neg_nat

deleted theorem sinZeta_two_mul_nat_add_one'

deleted theorem sinZeta_two_mul_nat_add_one