ZetaValues

📁 Source: Mathlib/NumberTheory/ZetaValues.lean

Statistics

Metric	Count
Definitions bernoulliFourierCoeff, bernoulliFun, periodizedBernoulli	3
Theorems antideriv_bernoulliFun, bernoulliFourierCoeff_eq, bernoulliFourierCoeff_recurrence, bernoulliFourierCoeff_zero, bernoulliFun_endpoints_eq_of_ne_one, bernoulliFun_eq_integral, bernoulliFun_eval_half, bernoulliFun_eval_half_eq_zero, bernoulliFun_eval_one, bernoulliFun_eval_one_sub, bernoulliFun_eval_zero, bernoulliFun_mul, bernoulliFun_one, bernoulliFun_two, bernoulliFun_zero, bernoulli_zero_fourier_coeff, contDiff_bernoulliFun, continuous_bernoulliFun, deriv_bernoulliFun, fourierCoeff_bernoulli_eq, hasDerivAt_bernoulliFun, hasSum_L_function_mod_four_eval_three, hasSum_one_div_nat_pow_mul_cos, hasSum_one_div_nat_pow_mul_fourier, hasSum_one_div_nat_pow_mul_sin, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, hasSum_zeta_four, hasSum_zeta_nat, hasSum_zeta_two, integral_bernoulliFun, integral_bernoulliFun_eq_zero, intervalIntegrable_bernoulliFun, continuous, summable_bernoulli_fourier	34
Total	37

(root)

Definitions

Name	Category	Theorems
bernoulliFourierCoeff 📖	CompOp	4 math math: bernoulliFourierCoeff_zero, bernoulli_zero_fourier_coeff, bernoulliFourierCoeff_eq, bernoulliFourierCoeff_recurrence
bernoulliFun 📖	CompOp	21 math math: bernoulliFun_eval_one_sub, intervalIntegrable_bernoulliFun, bernoulliFun_eval_half_eq_zero, hasDerivAt_bernoulliFun, bernoulliFun_two, hasSum_one_div_nat_pow_mul_fourier, antideriv_bernoulliFun, integral_bernoulliFun, bernoulliFun_eval_one, integral_bernoulliFun_eq_zero, bernoulliFun_endpoints_eq_of_ne_one, contDiff_bernoulliFun, continuous_bernoulliFun, bernoulliFun_eval_zero, bernoulliFun_zero, bernoulliFun_one, bernoulliFun_mul, bernoulliFun_eq_integral, deriv_bernoulliFun, hasSum_one_div_pow_mul_fourier_mul_bernoulliFun, bernoulliFun_eval_half
periodizedBernoulli 📖	CompOp	2 math math: fourierCoeff_bernoulli_eq, periodizedBernoulli.continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antideriv_bernoulliFun 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal DivInvMonoid.toDiv Real.instDivInvMonoid bernoulliFun Real.instNatCast Real.instOne	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Nat.cast_add Nat.cast_one add_tsub_cancel_right Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Nat.cast_add_one_ne_zero RCLike.charZero_rclike HasDerivAt.div_const hasDerivAt_bernoulliFun
bernoulliFourierCoeff_eq 📖	mathematical	—	bernoulliFourierCoeff Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.instNatCast Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instMul instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne bernoulliFourierCoeff_zero Int.cast_zero MulZeroClass.mul_zero zero_pow div_zero Nat.le_induction bernoulliFourierCoeff_recurrence neg_mul Nat.cast_one tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub one_mul pow_one bernoulli_zero_fourier_coeff sub_zero mul_one div_neg neg_div Nat.factorial_succ zero_sub Nat.cast_mul pow_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.instAtLeastTwo 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.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.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsRat.to_raw_eq Mathlib.Meta.NormNum.isRat_inv_neg Complex.instCharZero Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero 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.IsInt.to_isNat Mathlib.Tactic.Ring.pow_one_cast Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
bernoulliFourierCoeff_recurrence 📖	mathematical	—	bernoulliFourierCoeff Complex Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Complex.instSub Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike fourierCoeffOn_of_hasDerivAt HasDerivAt.ofReal_comp hasDerivAt_bernoulliFun Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp Complex.continuous_ofReal Continuous.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_const Polynomial.continuous sub_zero one_mul AddSubgroup.normal_of_comm QuotientAddGroup.mk_zero fourier_eval_zero Complex.ofReal_sub bernoulliFun_eval_one add_sub_cancel_left fourierCoeffOn.congr_simp Complex.ofReal_mul fourierCoeffOn.const_mul
bernoulliFourierCoeff_zero 📖	mathematical	—	bernoulliFourierCoeff Complex Complex.instZero	—	fourierCoeffOn_eq_integral neg_zero fourier_zero sub_zero div_one one_smul intervalIntegral.integral_ofReal integral_bernoulliFun_eq_zero
bernoulliFun_endpoints_eq_of_ne_one 📖	mathematical	—	bernoulliFun Real Real.instOne Real.instZero	—	bernoulliFun_eval_zero RCLike.charZero_rclike bernoulliFun.eq_1 Polynomial.eval_one_map Polynomial.bernoulli_eval_one bernoulli_eq_bernoulli'_of_ne_one eq_ratCast RingHom.instRingHomClass
bernoulliFun_eq_integral 📖	mathematical	—	bernoulliFun Real Real.instAdd intervalIntegral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instMul Real.instNatCast MeasureTheory.MeasureSpace.volume Real.measureSpace	—	intervalIntegral.integral_eq_sub_of_hasDerivAt Real.instCompleteSpace hasDerivAt_bernoulliFun Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuous_const continuous_id' continuous_bernoulliFun add_sub_cancel
bernoulliFun_eval_half 📖	mathematical	—	bernoulliFun Real Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instMul Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instOne Real.instRatCast bernoulli	—	Nat.instAtLeastTwoHAddOfNat bernoulliFun_one one_div sub_self pow_one div_self RCLike.charZero_rclike bernoulli_one Rat.cast_div Rat.cast_neg Rat.cast_one Rat.cast_ofNat MulZeroClass.zero_mul bernoulliFun_mul two_ne_zero inv_div sub_one_mul sub_eq_iff_eq_add inv_mul_eq_iff_eq_mul₀ ne_of_gt div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing pow_pos IsStrictOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo zero_add add_zero zero_div bernoulliFun_eval_zero bernoulliFun_eval_one add_halves ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.cast_one Nat.cast_zero Finset.sum_range_zero Finset.sum_range_succ mul_inv_cancel₀ two_ne_zero' Finset.sum_congr
bernoulliFun_eval_half_eq_zero 📖	mathematical	—	bernoulliFun Real Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instZero	—	Nat.instAtLeastTwoHAddOfNat bernoulliFun_eval_one_sub Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.lt_of_eq_of_lt neg_eq_zero Mathlib.Tactic.Linarith.without_one_mul CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike CancelDenoms.sub_subst CancelDenoms.neg_subst sub_eq_zero_of_eq sub_eq_of_eq_add add_halves ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid pow_succ Even.neg_pow Distrib.rightDistribClass one_pow mul_neg mul_one neg_mul one_mul Mathlib.Tactic.Linarith.mul_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true
bernoulliFun_eval_one 📖	mathematical	—	bernoulliFun Real Real.instOne Real.instAdd Real.instZero	—	RCLike.charZero_rclike bernoulliFun.eq_1 bernoulliFun_eval_zero Polynomial.eval_one_map Polynomial.bernoulli_eval_one bernoulli_one bernoulli'_one eq_ratCast RingHom.instRingHomClass Nat.instAtLeastTwoHAddOfNat Rat.cast_div Rat.cast_one Rat.cast_ofNat Rat.cast_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq 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 Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.add_pf_zero_add bernoulli_eq_bernoulli'_of_ne_one add_zero
bernoulliFun_eval_one_sub 📖	mathematical	—	bernoulliFun Real Real.instSub Real.instOne Real.instMul Monoid.toNatPow Real.instMonoid Real.instNeg	—	RCLike.charZero_rclike Polynomial.eval_map_algebraMap Polynomial.aeval_comp Polynomial.aeval_sub map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval_X map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_pow Polynomial.aeval_neg Polynomial.bernoulli_comp_one_sub_X
bernoulliFun_eval_zero 📖	mathematical	—	bernoulliFun Real Real.instZero Real.instRatCast bernoulli	—	RCLike.charZero_rclike bernoulliFun.eq_1 Polynomial.eval_zero_map Polynomial.bernoulli_eval_zero eq_ratCast RingHom.instRingHomClass
bernoulliFun_mul 📖	mathematical	—	bernoulliFun Real Real.instMul Real.instNatCast DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Finset.sum Real.instAddCommMonoid Finset.range Real.instAdd	—	Nat.cast_ne_zero RCLike.charZero_rclike bernoulliFun_zero pow_zero one_div Finset.sum_congr Finset.sum_const Finset.card_range nsmul_eq_mul mul_one inv_mul_cancel₀ IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal HasDerivAt.congr_simp Finset.mul_sum pow_succ mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass mul_sub mul_comm div_mul_cancel₀ HasDerivAt.sub IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mul_assoc Nat.cast_add_one HasDerivAt.comp hasDerivAt_bernoulliFun hasDerivAt_const_mul HasDerivAt.fun_sum HasDerivAt.const_mul HasDerivAt.add_const hasDerivAt_id' is_const_of_deriv_eq_zero HasDerivAt.differentiableAt MulZeroClass.mul_zero HasDerivAt.deriv intervalIntegral.integral_sub Continuous.intervalIntegrable Real.locallyFinite_volume Continuous.comp' continuous_bernoulliFun Continuous.fun_mul IsTopologicalSemiring.toContinuousMul continuous_const continuous_id' continuous_finset_sum IsTopologicalSemiring.toContinuousAdd Continuous.fun_add intervalIntegral.integral_comp_mul_left mul_inv_cancel₀ integral_bernoulliFun_eq_zero smul_zero sub_eq_zero intervalIntegral.integral_const_mul mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass intervalIntegral.integral_finset_sum intervalIntegral.integral_comp_add_right zero_add add_comm intervalIntegral.sum_integral_adjacent_intervals CharP.cast_eq_zero CharP.ofCharZero zero_div div_self intervalIntegral.integral_const Real.instCompleteSpace sub_zero
bernoulliFun_one 📖	mathematical	—	bernoulliFun Real Real.instSub DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike Polynomial.bernoulli_def Finset.sum_range_succ Finset.sum_singleton tsub_zero Nat.instOrderedSub bernoulli_one Nat.choose_succ_self_right zero_add Nat.cast_one mul_one tsub_self Nat.instCanonicallyOrderedAdd bernoulli_zero Nat.choose_self Polynomial.map_add Polynomial.map_C map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_ratCast Rat.cast_neg Rat.cast_one Rat.cast_ofNat Polynomial.map_monomial Polynomial.eval_add Polynomial.eval_C Polynomial.eval_monomial pow_one one_mul one_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.div_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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsRat.to_raw_eq 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 Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt
bernoulliFun_two 📖	mathematical	—	bernoulliFun Real Real.instAdd Real.instSub Monoid.toNatPow Real.instMonoid Real.instInv instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike Polynomial.bernoulli_def Finset.sum_range_succ Finset.sum_singleton tsub_zero Nat.instOrderedSub bernoulli_two Nat.choose_zero_right Nat.cast_one mul_one bernoulli_one Nat.choose_succ_self_right IsUnit.div_mul_cancel Rat.instCharZero Polynomial.monomial_neg tsub_self Nat.instCanonicallyOrderedAdd bernoulli_zero Nat.choose_self Polynomial.map_add Polynomial.map_C map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_ratCast Rat.cast_ofNat Polynomial.map_neg Polynomial.map_monomial Rat.cast_one Polynomial.eval_add Polynomial.eval_C Polynomial.eval_neg Polynomial.eval_monomial pow_one one_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add 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 Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt
bernoulliFun_zero 📖	mathematical	—	bernoulliFun Real Real.instOne	—	RCLike.charZero_rclike Polynomial.bernoulli_zero Polynomial.map_one Polynomial.eval_one
bernoulli_zero_fourier_coeff 📖	mathematical	—	bernoulliFourierCoeff Complex Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat neg_mul one_div inv_neg mul_inv_rev Complex.inv_I mul_neg neg_neg CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub MulZeroClass.zero_mul sub_self MulZeroClass.mul_zero bernoulliFourierCoeff_recurrence
contDiff_bernoulliFun 📖	mathematical	—	ContDiff Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Top.top WithTop ENat WithTop.top bernoulliFun	—	RCLike.charZero_rclike Polynomial.eval_map_algebraMap
continuous_bernoulliFun 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace bernoulliFun	—	Polynomial.continuous_aeval IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal RCLike.charZero_rclike
deriv_bernoulliFun 📖	mathematical	—	deriv Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace bernoulliFun Real.instMul Real.instNatCast	—	HasDerivAt.deriv hasDerivAt_bernoulliFun
fourierCoeff_bernoulli_eq 📖	mathematical	—	fourierCoeff Real Real.instOne ZeroLEOneClass.factZeroLtOne Real.instZero Real.partialOrder Real.instZeroLEOneClass NeZero.charZero_one AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instRing RCLike.charZero_rclike Real.instRCLike Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace UnitAddCircle Complex.ofReal periodizedBernoulli DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.instNatCast Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instMul instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.pi Complex.I Complex.instIntCast	—	Real.instIsOrderedAddMonoid ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Real.instArchimedean Nat.instAtLeastTwoHAddOfNat lt_add_of_pos_right IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Fact.out fourierCoeff_liftIco_eq zero_add fourierCoeffOn.congr_simp bernoulliFourierCoeff_eq
hasDerivAt_bernoulliFun 📖	mathematical	—	HasDerivAt Real DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instAddCommGroup NormedSpace.toModule Real.normedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing InnerProductSpace.toNormedSpace Real.instRCLike RCLike.toInnerProductSpaceReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace IsModuleTopology.toContinuousSMul SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Real.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Real.semiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing instIsTopologicalRingReal bernoulliFun Real.instMul Real.instNatCast	—	IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.charZero_rclike Polynomial.derivative_map Polynomial.derivative_bernoulli Polynomial.map_mul Polynomial.map_natCast Polynomial.eval_mul Polynomial.eval_natCast Polynomial.hasDerivAt
hasSum_L_function_mod_four_eval_three 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Monoid.toNatPow Real.instMonoid Real.instNatCast Real.sin Real.pi instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add 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 Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.nnrat_rawCast Mathlib.Tactic.RingNF.mul_assoc_rev add_zero mul_one one_div map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_ratCast Rat.cast_ofNat mul_pow Polynomial.eval_map Polynomial.eval₂_at_apply Polynomial.bernoulli_three_eval_one_quarter Even.neg_pow one_pow one_mul zero_add map_div₀ Mathlib.Tactic.Ring.of_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1 hasSum_one_div_nat_pow_mul_sin one_ne_zero Set.mem_Icc le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.neg_congr 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_neg Real.instIsStrictOrderedRing neg_neg_of_pos Real.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one CancelDenoms.derive_trans Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_div CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true
hasSum_one_div_nat_pow_mul_cos 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instNatCast Real.cos instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.pi Real.instNeg Nat.factorial Polynomial.eval Real.semiring Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra Real.instDivisionRing RCLike.charZero_rclike Real.instRCLike Polynomial.bernoulli SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat pow_mul neg_one_sq one_pow one_mul pow_add pow_one mul_pow Complex.I_sq Mathlib.Tactic.Ring.of_eq 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 Nat.cast_one 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.atom_pf Mathlib.Tactic.Ring.pow_add 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.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.neg_mul hasSum_one_div_nat_pow_mul_fourier RCLike.charZero_rclike Complex.ofReal_mul mul_div Complex.ofReal_div Complex.ofReal_one Complex.ofReal_pow Complex.ofReal_cos fourier_coe_apply Complex.cos.eq_1 div_one Int.cast_neg Int.cast_natCast Complex.ofReal_natCast Complex.ofReal_re Complex.ofReal_neg bernoulliFun.eq_1 Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast 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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.IsRat.to_raw_eq 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 Complex.hasSum_iff HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
hasSum_one_div_nat_pow_mul_fourier 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNatCast Complex.instAdd DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier Complex.instNeg instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Nat.factorial bernoulliFun SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Int.cast_neg mul_add Distrib.leftDistribClass mul_assoc neg_eq_neg_one_mul mul_pow div_div div_mul_eq_mul_div₀ one_mul eq_div_iff pow_ne_zero isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass neg_ne_zero one_ne_zero NeZero.charZero_one Complex.instCharZero neg_neg one_pow Int.cast_zero zero_pow ne_of_gt lt_of_lt_of_le Mathlib.Meta.Positivity.pos_of_isNat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat div_zero MulZeroClass.zero_mul add_zero HasSum.nat_add_neg IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_one_div_pow_mul_fourier_mul_bernoulliFun
hasSum_one_div_nat_pow_mul_sin 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid Real.instNatCast Real.sin instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.pi Real.instNeg Nat.factorial Polynomial.eval Real.semiring Polynomial.map CommSemiring.toSemiring Rat.commSemiring algebraMap DivisionRing.toRatAlgebra Real.instDivisionRing RCLike.charZero_rclike Real.instRCLike Polynomial.bernoulli SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat pow_add pow_mul neg_one_sq one_pow one_mul pow_one neg_eq_neg_one_mul sub_eq_add_neg mul_pow Complex.I_sq Mathlib.Tactic.Ring.of_eq 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 Nat.cast_one 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.atom_pf Mathlib.Tactic.Ring.pow_add 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.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.neg_mul hasSum_one_div_nat_pow_mul_fourier RCLike.charZero_rclike Complex.ofReal_mul mul_div Complex.ofReal_div Complex.ofReal_one Complex.ofReal_pow Complex.ofReal_sin fourier_coe_apply Complex.sin.eq_1 div_one Int.cast_neg Int.cast_natCast Complex.ofReal_natCast div_div Complex.div_I div_mul_eq_mul_div₀ neg_div neg_mul neg_sub Complex.ofReal_re Complex.ofReal_neg Mathlib.Tactic.Ring.div_congr 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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_pow bernoulliFun.eq_1 Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.IsNNRat.to_isRat Complex.hasSum_iff HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
hasSum_one_div_pow_mul_fourier_mul_bernoulliFun 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instIntCast DFunLike.coe ContinuousMap AddCircle Real.instAddCommGroup QuotientAddGroup.instTopologicalSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup AddSubgroup.zmultiples ContinuousMap.instFunLike fourier Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Nat.factorial bernoulliFun SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Continuous.comp Complex.continuous_ofReal periodizedBernoulli.continuous ZeroLEOneClass.factZeroLtOne Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike fourierCoeff_bernoulli_eq has_pointwise_sum_fourier_series_of_summable Summable.congr summable_bernoulli_fourier smul_eq_mul mul_assoc mul_div mul_neg div_mul_cancel₀ Nat.cast_ne_zero Complex.instCharZero Nat.factorial_ne_zero neg_neg mul_pow div_div div_self pow_eq_zero_iff' isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instNontrivial not_and_or Complex.two_pi_I_ne_zero Real.instIsOrderedAddMonoid Real.instArchimedean periodizedBernoulli.eq_1 AddCircle.liftIco_coe_apply zero_add HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Set.mem_insert_iff Set.Ico_insert_right zero_le_one' AddCircle.coe_period AddSubgroup.normal_of_comm QuotientAddGroup.mk_zero bernoulliFun_endpoints_eq_of_ne_one Set.left_mem_Ico zero_lt_one
hasSum_zeta_four 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Monoid.toNatPow Real.instMonoid Real.instNatCast Real.pi instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.intPow_negOfNat_bit1 Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_natSub Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit1 Mathlib.Meta.NormNum.IsNat.to_eq neg_mul bernoulli_eq_bernoulli'_of_ne_one bernoulli'_four Rat.cast_div RCLike.charZero_rclike Rat.cast_neg Rat.cast_one Rat.cast_ofNat zero_add mul_one Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos 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 Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.IsRat.to_raw_eq 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 Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz Mathlib.Tactic.Ring.neg_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul hasSum_zeta_nat two_ne_zero
hasSum_zeta_nat 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Monoid.toNatPow Real.instMonoid Real.instNatCast Real.instMul Real.instNeg instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Real.pi Real.instRatCast bernoulli Nat.factorial SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat RCLike.charZero_rclike MulZeroClass.mul_zero Real.cos_zero mul_one Polynomial.eval_zero_map Polynomial.bernoulli_eval_zero eq_ratCast RingHom.instRingHomClass eq_div_iff two_ne_zero' ZeroLEOneClass.neZero.two Real.instZeroLEOneClass NeZero.charZero_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid pow_one pow_add mul_pow 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 Nat.cast_one 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.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsRat.to_raw_eq 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 Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat hasSum_one_div_nat_pow_mul_cos Set.left_mem_Icc zero_le_one
hasSum_zeta_two 📖	mathematical	—	HasSum Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Monoid.toNatPow Real.instMonoid Real.instNatCast Real.pi instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat mul_one bernoulli_eq_bernoulli'_of_ne_one bernoulli'_two Even.neg_pow one_pow pow_one one_mul one_div Rat.cast_inv RCLike.charZero_rclike Rat.cast_ofNat zero_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat 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 Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.inv_congr Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz hasSum_zeta_nat one_ne_zero
integral_bernoulliFun 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal bernoulliFun Real.instZero Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace	—	intervalIntegral.integral_eq_sub_of_hasDerivAt Real.instCompleteSpace antideriv_bernoulliFun intervalIntegrable_bernoulliFun bernoulliFun_eval_one add_sub_cancel_left ite_div CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike zero_add div_self NeZero.charZero_one zero_div
integral_bernoulliFun_eq_zero 📖	mathematical	—	intervalIntegral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal bernoulliFun Real.instZero Real.instOne MeasureTheory.MeasureSpace.volume Real.measureSpace	—	integral_bernoulliFun
intervalIntegrable_bernoulliFun 📖	mathematical	—	IntervalIntegrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace NormedAddGroup.toENormedAddMonoid NormedAddCommGroup.toNormedAddGroup Real.normedAddCommGroup bernoulliFun MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Continuous.intervalIntegrable Real.locallyFinite_volume continuous_bernoulliFun
summable_bernoulli_fourier 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.instNatCast Nat.factorial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instMul instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat mul_one_div div_div mul_pow Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Summable.of_norm Complex.instCompleteSpace one_div norm_inv norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Complex.norm_intCast pow_abs Real.instIsOrderedRing abs_inv Real.instIsStrictOrderedRing summable_abs_iff Real.instIsOrderedAddMonoid instIsUniformAddGroupReal Real.instCompleteSpace Real.summable_one_div_int_pow

periodizedBernoulli

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous 📖	mathematical	—	Continuous UnitAddCircle Real QuotientAddGroup.instTopologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne periodizedBernoulli	—	AddCircle.liftIco_zero_continuous Real.instIsOrderedAddMonoid Real.instArchimedean instOrderTopologyReal Nat.cast_zero Nat.cast_one bernoulliFun_endpoints_eq_of_ne_one Continuous.continuousOn RCLike.charZero_rclike Polynomial.continuous IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal

---

← Back to Index