Commit 2023-06-29 08:26 584c909a

View on Github →

feat: port NumberTheory.ZetaFunction (#5556)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/ZetaFunction.lean

added def RiemannHypothesis

added theorem completed_zeta_eq_mellin_of_one_lt_re

added theorem completed_zeta_eq_tsum_of_one_lt_re

added theorem continuousAt_zetaKernel₁

added theorem differentiableAt_completed_zeta

added theorem differentiableAt_mellin_zetaKernel₁

added theorem differentiableAt_riemannZeta

added theorem differentiable_completed_zeta₀

added theorem differentiable_mellin_zetaKernel₂

added theorem hasMellin_one_div_sqrt_Ioc

added theorem hasMellin_one_div_sqrt_sub_one_div_two_Ioc

added theorem integral_cpow_mul_exp_neg_pi_mul_sq

added theorem isBigO_atTop_zetaKernel₁

added theorem isBigO_atTop_zetaKernel₂

added theorem isBigO_zero_zetaKernel₁

added theorem isBigO_zero_zetaKernel₂

added theorem isBigO_zero_zetaKernel₂_rpow

added theorem locally_integrable_zetaKernel₁

added theorem locally_integrable_zetaKernel₂

added theorem mellin_zetaKernel₁_eq_tsum

added theorem mellin_zetaKernel₂_eq_of_lt_re

added def riemannCompletedZeta

added theorem riemannCompletedZeta_one_sub

added def riemannCompletedZeta₀

added theorem riemannCompletedZeta₀_one_sub

added theorem riemannZeta_four

added theorem riemannZeta_neg_nat_eq_bernoulli

added theorem riemannZeta_neg_two_mul_nat_add_one

added theorem riemannZeta_one_sub

added theorem riemannZeta_two

added theorem riemannZeta_two_mul_nat

added theorem riemannZeta_zero

added theorem summable_exp_neg_pi_mul_nat_sq

added def zetaKernel₁

added theorem zetaKernel₁_eq_jacobiTheta

added def zetaKernel₂

added theorem zetaKernel₂_one_div

added theorem zeta_eq_tsum_one_div_nat_add_one_cpow

added theorem zeta_eq_tsum_one_div_nat_cpow

added theorem zeta_nat_eq_tsum_of_gt_one