HurwitzZetaValues

📁 Source: Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean

Statistics

Metric	Count
Definitions	0
Theorems cosZeta_two_mul_nat, cosZeta_two_mul_nat', hurwitzZetaEven_one_sub_two_mul_nat, hurwitzZetaOdd_neg_two_mul_nat, hurwitzZeta_neg_nat, sinZeta_two_mul_nat_add_one, sinZeta_two_mul_nat_add_one', riemannZeta_four, riemannZeta_neg_nat_eq_bernoulli, riemannZeta_neg_nat_eq_bernoulli', riemannZeta_two, riemannZeta_two_mul_nat	12
Total	12

HurwitzZeta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cosZeta_two_mul_nat 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	cosZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Complex Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.ofReal Real.pi Nat.factorial Polynomial.eval Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.bernoulli	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional hasSum_nat_cosZeta Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Complex.ofReal_tsum tsum_congr Complex.cpow_natCast Nat.cast_pow Complex.ofReal_pow Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mul_one Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasSum_one_div_nat_pow_mul_cos Complex.ofReal_mul Complex.ofReal_div Complex.ofReal_neg Polynomial.map_map Complex.ofRealHom_eq_coe Polynomial.map_aeval_eq_aeval_map RingHomCompTriple.comp_eq RingHomCompTriple.right_ids RingHomCompTriple.ids
cosZeta_two_mul_nat' 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	cosZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Complex Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.Gammaℂ Polynomial.eval Complex.ofReal Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.bernoulli	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero cosZeta_two_mul_nat Nat.cast_one Complex.Gamma_nat_eq_factorial Nat.cast_add_one Nat.cast_mul Nat.factorial_succ Complex.cpow_neg div_inv_eq_mul div_mul_eq_mul_div div_div mul_right_comm Int.cast_pow Int.cast_neg Int.cast_one Complex.ofReal_pow Complex.ofReal_neg Complex.cpow_natCast
hurwitzZetaEven_one_sub_two_mul_nat 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	hurwitzZetaEven AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Complex Complex.instSub Complex.instOne Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Polynomial.eval Complex.instSemiring Complex.ofReal Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.bernoulli	—	Nat.instAtLeastTwoHAddOfNat Int.cast_ofNat Int.cast_natCast Int.cast_mul Int.cast_neg Complex.instCharZero ne_of_gt LE.le.trans_lt neg_nonpos_of_nonneg Int.instIsOrderedAddMonoid Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing mul_pos IsStrictOrderedRing.toPosMulStrictMono two_pos Int.instZeroLEOneClass Int.instAddLeftMono Nat.cast_pos Int.instNontrivial Nat.cast_one Unique.instSubsingleton Nat.instCharZero mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass two_ne_zero CharZero.NeZero.two Complex.Gamma_ne_zero hurwitzZetaEven_one_sub Complex.Gammaℂ.eq_1 cosZeta_two_mul_nat' mul_assoc mul_div_assoc mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Complex.ofReal_natCast Complex.ofReal_mul Complex.ofReal_cos mul_comm sub_zero Real.cos_nat_mul_pi_sub Real.cos_zero mul_one Complex.ofReal_pow Complex.ofReal_neg Complex.ofReal_one pow_succ mul_neg_one mul_neg mul_pow neg_one_mul neg_neg one_pow
hurwitzZetaOdd_neg_two_mul_nat 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	hurwitzZetaOdd AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Complex Complex.instNeg Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instAdd Polynomial.eval Complex.instSemiring Complex.ofReal Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.bernoulli	—	Nat.instAtLeastTwoHAddOfNat Int.cast_ofNat Int.cast_natCast Int.cast_mul Int.cast_neg Int.cast_one Int.cast_add Complex.instCharZero ne_of_gt LE.le.trans_lt neg_nonpos_of_nonneg Int.instIsOrderedAddMonoid Nat.cast_nonneg IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing add_pos' Int.instAddLeftMono mul_pos IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Int.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_pos' Int.instZeroLEOneClass lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass two_ne_zero CharZero.NeZero.two neg_add_rev Complex.Gamma_ne_zero sub_add_cancel_right hurwitzZetaOdd_one_sub Complex.Gammaℂ.eq_1 sinZeta_two_mul_nat_add_one' mul_assoc mul_div_assoc mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass add_div Complex.ofReal_natCast Complex.ofReal_one Complex.ofReal_ofNat Complex.ofReal_div Complex.ofReal_add Complex.ofReal_mul Complex.ofReal_sin mul_comm add_mul Distrib.rightDistribClass mul_one_div Real.sin_add_pi_div_two sub_zero Real.cos_nat_mul_pi_sub Real.cos_zero mul_one Complex.ofReal_pow Complex.ofReal_neg pow_succ mul_neg_one mul_neg mul_pow neg_one_mul neg_neg one_pow
hurwitzZeta_neg_nat 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	hurwitzZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Complex Complex.instNeg Complex.instNatCast Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instAdd Polynomial.eval Complex.instSemiring Complex.ofReal Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.bernoulli	—	Complex.instCharZero Nat.even_or_odd' Nat.instAtLeastTwoHAddOfNat Nat.cast_one Nat.cast_add Nat.cast_mul Int.cast_add Int.cast_mul Int.cast_ofNat Int.cast_natCast Int.cast_one
sinZeta_two_mul_nat_add_one 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	sinZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Complex Complex.instAdd Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instOne DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.ofReal Real.pi Nat.factorial Polynomial.eval Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.bernoulli	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional hasSum_nat_sinZeta Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Complex.ofReal_tsum tsum_congr Complex.cpow_natCast Nat.cast_pow Complex.ofReal_pow Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero mul_one Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasSum_one_div_nat_pow_mul_sin Complex.ofReal_mul Complex.ofReal_div Complex.ofReal_neg Polynomial.map_map Complex.ofRealHom_eq_coe Polynomial.map_aeval_eq_aeval_map RingHomCompTriple.comp_eq RingHomCompTriple.right_ids RingHomCompTriple.ids
sinZeta_two_mul_nat_add_one' 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	sinZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Complex Complex.instAdd Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instOne DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.Gammaℂ Polynomial.eval Complex.ofReal Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Complex.instNormedField Complex.instCharZero Polynomial.bernoulli	—	Nat.instAtLeastTwoHAddOfNat Complex.instCharZero sinZeta_two_mul_nat_add_one Nat.cast_mul Complex.Gamma_nat_eq_factorial Nat.cast_ofNat Nat.cast_add_one Nat.factorial_succ Complex.cpow_neg div_inv_eq_mul div_mul_eq_mul_div div_div Nat.cast_add Nat.cast_one Complex.cpow_natCast Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
riemannZeta_four 📖	mathematical	—	riemannZeta Complex instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_one zeta_nat_eq_tsum_of_gt_one IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero Complex.ofReal_tsum Complex.ofReal_div Complex.ofReal_pow HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_zeta_four
riemannZeta_neg_nat_eq_bernoulli 📖	mathematical	—	riemannZeta Complex Complex.instNeg Complex.instNatCast DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instOne Complex.instRatCast bernoulli Complex.instAdd	—	riemannZeta_neg_nat_eq_bernoulli' bernoulli.eq_1 Rat.cast_mul Complex.instCharZero Rat.cast_pow Rat.cast_neg Rat.cast_one neg_one_mul mul_assoc pow_succ mul_pow neg_neg one_pow one_mul
riemannZeta_neg_nat_eq_bernoulli' 📖	mathematical	—	riemannZeta Complex Complex.instNeg Complex.instNatCast DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instRatCast bernoulli' Complex.instAdd Complex.instOne	—	eq_or_ne Nat.cast_zero neg_zero Nat.instAtLeastTwoHAddOfNat riemannZeta_zero zero_add div_one bernoulli'_one Rat.cast_div Complex.instCharZero Rat.cast_one Rat.cast_ofNat neg_div HurwitzZeta.hurwitzZeta_zero AddSubgroup.normal_of_comm QuotientAddGroup.mk_zero HurwitzZeta.hurwitzZeta_neg_nat Set.left_mem_Icc zero_le_one Real.instZeroLEOneClass Complex.ofReal_zero Polynomial.eval_zero_map Polynomial.bernoulli_eval_zero Algebra.algebraMap_eq_smul_one Rat.smul_one_eq_cast div_mul_eq_mul_div neg_one_mul bernoulli_eq_bernoulli'_of_ne_one
riemannZeta_two 📖	mathematical	—	riemannZeta Complex instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.ofReal Real.pi	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_two zeta_nat_eq_tsum_of_gt_one one_lt_two Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid one_div Complex.ofReal_tsum Complex.ofReal_inv Complex.ofReal_pow HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_zeta_two
riemannZeta_two_mul_nat 📖	mathematical	—	riemannZeta Complex Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.instOne Complex.ofReal Real.pi Complex.instRatCast bernoulli Nat.factorial	—	Nat.instAtLeastTwoHAddOfNat Nat.cast_two Nat.cast_mul zeta_nat_eq_tsum_of_gt_one one_div Complex.ofReal_tsum Complex.ofReal_inv Complex.ofReal_pow Nat.cast_one Nat.cast_pow Int.cast_pow Int.cast_ofNat Int.cast_mul Int.cast_neg Int.cast_one Complex.ofReal_mul Complex.ofReal_neg HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_zeta_nat

---

← Back to Index