Commit 2023-06-21 07:53 4a2172e7

View on Github →

feat: port NumberTheory.ZetaValues (#5300)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/PSeries.lean

modified theorem Real.summable_nat_pow_inv

modified theorem Real.summable_nat_rpow

modified theorem Real.summable_nat_rpow_inv

modified theorem Real.summable_one_div_nat_pow

modified theorem Real.summable_one_div_nat_rpow

modified theorem sum_Ioo_inv_sq_le

Created Mathlib/NumberTheory/ZetaValues.lean

added theorem Polynomial.bernoulli_three_eval_one_quarter

added theorem antideriv_bernoulliFun

added def bernoulliFourierCoeff

added theorem bernoulliFourierCoeff_eq

added theorem bernoulliFourierCoeff_recurrence

added theorem bernoulliFourierCoeff_zero

added def bernoulliFun

added theorem bernoulliFun_endpoints_eq_of_ne_one

added theorem bernoulliFun_eval_one

added theorem bernoulliFun_eval_zero

added theorem bernoulli_zero_fourier_coeff

added theorem fourierCoeff_bernoulli_eq

added theorem hasDerivAt_bernoulliFun

added theorem hasSum_L_function_mod_four_eval_three

added theorem hasSum_one_div_nat_pow_mul_cos

added theorem hasSum_one_div_nat_pow_mul_fourier

added theorem hasSum_one_div_nat_pow_mul_sin

added theorem hasSum_one_div_pow_mul_fourier_mul_bernoulliFun

added theorem hasSum_zeta_four

added theorem hasSum_zeta_nat

added theorem hasSum_zeta_two

added theorem integral_bernoulliFun_eq_zero

added theorem periodizedBernoulli.continuous

added def periodizedBernoulli

added theorem summable_bernoulli_fourier