HurwitzZetaEven

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

Statistics

Metric	Count
Definitions completedCosZeta, completedCosZeta₀, completedHurwitzZetaEven, completedHurwitzZetaEven₀, cosKernel, cosZeta, evenKernel, hurwitzEvenFEPair, hurwitzZetaEven	9
Theorems LSeriesHasSum_cos, completedCosZeta_eq, completedCosZeta_neg, completedCosZeta_one_sub, completedCosZeta_residue_zero, completedCosZeta₀_neg, completedCosZeta₀_one_sub, completedHurwitzZetaEven_eq, completedHurwitzZetaEven_neg, completedHurwitzZetaEven_one_sub, completedHurwitzZetaEven_residue_one, completedHurwitzZetaEven_residue_zero, completedHurwitzZetaEven₀_neg, completedHurwitzZetaEven₀_one_sub, continuousOn_cosKernel, continuousOn_evenKernel, cosKernel_def, cosKernel_neg, cosKernel_undef, cosZeta_apply_zero, cosZeta_neg, cosZeta_neg_two_mul_nat_add_one, cosZeta_one_sub, differentiableAt_completedCosZeta, differentiableAt_completedHurwitzZetaEven, differentiableAt_cosZeta, differentiableAt_hurwitzZetaEven, differentiableAt_hurwitzZetaEven_sub_one_div, differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven, differentiableAt_update_of_residue, differentiable_completedCosZeta₀, differentiable_completedHurwitzZetaEven₀, differentiable_cosZeta_of_ne_zero, differentiable_hurwitzZetaEven_sub_hurwitzZetaEven, evenKernel_def, evenKernel_eq_cosKernel_of_zero, evenKernel_functional_equation, evenKernel_neg, evenKernel_undef, hasSum_int_completedCosZeta, hasSum_int_completedHurwitzZetaEven, hasSum_int_cosKernel, hasSum_int_cosKernel₀, hasSum_int_cosZeta, hasSum_int_evenKernel, hasSum_int_evenKernel₀, hasSum_int_hurwitzZetaEven, hasSum_nat_completedCosZeta, hasSum_nat_cosKernel₀, hasSum_nat_cosZeta, hasSum_nat_hurwitzZetaEven, hasSum_nat_hurwitzZetaEven_of_mem_Icc, hurwitzEvenFEPair_neg, hurwitzEvenFEPair_zero_symm, hurwitzZetaEven_apply_zero, hurwitzZetaEven_def_of_ne_or_ne, hurwitzZetaEven_neg, hurwitzZetaEven_neg_two_mul_nat_add_one, hurwitzZetaEven_one_sub, hurwitzZetaEven_residue_one, isBigO_atTop_cosKernel_sub, isBigO_atTop_evenKernel_sub, tendsto_hurwitzZetaEven_sub_one_div_nhds_one	63
Total	72

HurwitzZeta

Definitions

Name	Category	Theorems
completedCosZeta 📖	CompOp	9 math math: hasSum_nat_completedCosZeta, completedCosZeta_residue_zero, completedHurwitzZetaEven_one_sub, differentiableAt_completedCosZeta, completedCosZeta_eq, completedCosZeta_one_sub, completedCosZeta_zero, completedCosZeta_neg, hasSum_int_completedCosZeta
completedCosZeta₀ 📖	CompOp	6 math math: completedCosZeta₀_neg, completedCosZeta₀_zero, completedCosZeta₀_one_sub, completedCosZeta_eq, completedHurwitzZetaEven₀_one_sub, differentiable_completedCosZeta₀
completedHurwitzZetaEven 📖	CompOp	12 math math: hurwitzZetaEven_def_of_ne_or_ne, ZMod.completedLFunction_def_even, completedHurwitzZetaEven_residue_one, completedHurwitzZetaEven_eq, differentiableAt_completedHurwitzZetaEven, differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven, completedHurwitzZetaEven_one_sub, completedHurwitzZetaEven_zero, completedCosZeta_one_sub, completedHurwitzZetaEven_neg, completedHurwitzZetaEven_residue_zero, hasSum_int_completedHurwitzZetaEven
completedHurwitzZetaEven₀ 📖	CompOp	6 math math: completedHurwitzZetaEven_eq, completedCosZeta₀_one_sub, completedHurwitzZetaEven₀_neg, completedHurwitzZetaEven₀_zero, differentiable_completedHurwitzZetaEven₀, completedHurwitzZetaEven₀_one_sub
cosKernel 📖	CompOp	10 math math: hasSum_int_cosKernel₀, evenKernel_eq_cosKernel_of_zero, hasSum_int_cosKernel, continuousOn_cosKernel, cosKernel_def, cosKernel_undef, cosKernel_neg, evenKernel_functional_equation, isBigO_atTop_cosKernel_sub, hasSum_nat_cosKernel₀
cosZeta 📖	CompOp	14 math math: LSeriesHasSum_cos, cosZeta_two_mul_nat', cosZeta_two_mul_nat, cosZeta_neg_two_mul_nat_add_one, cosZeta_apply_zero, cosZeta_one_sub, cosZeta_eq, hasSum_int_cosZeta, hasSum_nat_cosZeta, hurwitzZetaEven_one_sub, cosZeta_zero, differentiable_cosZeta_of_ne_zero, cosZeta_neg, differentiableAt_cosZeta
evenKernel 📖	CompOp	9 math math: isBigO_atTop_evenKernel_sub, evenKernel_def, evenKernel_eq_cosKernel_of_zero, continuousOn_evenKernel, hasSum_int_evenKernel, evenKernel_neg, evenKernel_functional_equation, hasSum_int_evenKernel₀, evenKernel_undef
hurwitzEvenFEPair 📖	CompOp	2 math math: hurwitzEvenFEPair_zero_symm, hurwitzEvenFEPair_neg
hurwitzZetaEven 📖	CompOp	18 math math: differentiableAt_hurwitzZetaEven_sub_one_div, differentiableAt_hurwitzZetaEven, hasSum_int_hurwitzZetaEven, hurwitzZetaEven_def_of_ne_or_ne, hurwitzZetaEven_zero, hurwitzZetaEven_apply_zero, hasSum_nat_hurwitzZetaEven, cosZeta_one_sub, hurwitzZetaEven_neg_two_mul_nat_add_one, hurwitzZetaEven_one_sub, hurwitzZetaEven_one_sub_two_mul_nat, ZMod.LFunction_def_even, hasSum_nat_hurwitzZetaEven_of_mem_Icc, differentiable_hurwitzZetaEven_sub_hurwitzZetaEven, hurwitzZetaEven_neg, hurwitzZetaEven_eq, tendsto_hurwitzZetaEven_sub_one_div_nhds_one, hurwitzZetaEven_residue_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LSeriesHasSum_cos 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeriesHasSum Complex.ofReal Real.cos Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi cosZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples	—	HasSum.congr_fun Nat.instAtLeastTwoHAddOfNat hasSum_nat_cosZeta LSeries.term_of_ne_zero' Complex.ne_zero_of_one_lt_re
completedCosZeta_eq 📖	mathematical	—	completedCosZeta Complex Complex.instSub completedCosZeta₀ DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem AddSubgroup.decidableMemZMultiples Real.instAddGroup Complex.instZero	—	completedCosZeta.eq_1 WeakFEPair.Λ.eq_1 sub_div completedCosZeta₀.eq_1 WeakFEPair.hg_int WeakFEPair.hf_int WeakFEPair.hk WeakFEPair.h_feq' WeakFEPair.hg_top WeakFEPair.hf_top WeakFEPair.symm.eq_1 hurwitzEvenFEPair.eq_1 smul_eq_mul mul_one div_div Nat.instAtLeastTwoHAddOfNat div_mul_cancel₀ two_ne_zero' CharZero.NeZero.two Complex.instCharZero Complex.ofReal_div inv_one mul_comm mul_div_assoc mul_one_div
completedCosZeta_neg 📖	mathematical	—	completedCosZeta UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	hurwitzEvenFEPair_neg
completedCosZeta_one_sub 📖	mathematical	—	completedCosZeta Complex Complex.instSub Complex.instOne completedHurwitzZetaEven	—	completedHurwitzZetaEven_one_sub sub_sub_cancel
completedCosZeta_residue_zero 📖	mathematical	—	Filter.Tendsto Complex Complex.instMul completedCosZeta nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet nhds Complex.instNeg Complex.instOne	—	WeakFEPair.Λ_residue_zero Filter.Tendsto.congr Nat.instAtLeastTwoHAddOfNat div_mul_eq_mul_div mul_div_assoc Filter.Tendsto.comp zero_div
completedCosZeta₀_neg 📖	mathematical	—	completedCosZeta₀ UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	hurwitzEvenFEPair_neg
completedCosZeta₀_one_sub 📖	mathematical	—	completedCosZeta₀ Complex Complex.instSub Complex.instOne completedHurwitzZetaEven₀	—	completedHurwitzZetaEven₀_one_sub sub_sub_cancel
completedHurwitzZetaEven_eq 📖	mathematical	—	completedHurwitzZetaEven Complex Complex.instSub completedHurwitzZetaEven₀ DivInvMonoid.toDiv Complex.instDivInvMonoid UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem AddSubgroup.decidableMemZMultiples Real.instAddGroup Complex.instOne Complex.instZero	—	completedHurwitzZetaEven.eq_1 WeakFEPair.Λ.eq_1 sub_div Nat.instAtLeastTwoHAddOfNat smul_eq_mul mul_comm mul_div_assoc div_div div_mul_cancel₀ two_ne_zero CharZero.NeZero.two Complex.instCharZero mul_one_div Complex.ofReal_div mul_one
completedHurwitzZetaEven_neg 📖	mathematical	—	completedHurwitzZetaEven UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	hurwitzEvenFEPair_neg
completedHurwitzZetaEven_one_sub 📖	mathematical	—	completedHurwitzZetaEven Complex Complex.instSub Complex.instOne completedCosZeta	—	completedHurwitzZetaEven.eq_1 completedCosZeta.eq_1 sub_div Nat.instAtLeastTwoHAddOfNat one_div Complex.ofReal_inv WeakFEPair.functional_equation one_smul
completedHurwitzZetaEven_residue_one 📖	mathematical	—	Filter.Tendsto Complex Complex.instMul Complex.instSub Complex.instOne completedHurwitzZetaEven nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	Nat.instAtLeastTwoHAddOfNat WeakFEPair.Λ_residue_k Filter.Tendsto.congr completedHurwitzZetaEven.eq_1 sub_div div_mul_eq_mul_div mul_div_assoc Filter.Tendsto.comp Complex.ofReal_div one_mul
completedHurwitzZetaEven_residue_zero 📖	mathematical	—	Filter.Tendsto Complex Complex.instMul completedHurwitzZetaEven nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet nhds UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem AddSubgroup.decidableMemZMultiples Real.instAddGroup Complex.instNeg Complex.instOne	—	WeakFEPair.Λ_residue_zero neg_zero Filter.Tendsto.congr Nat.instAtLeastTwoHAddOfNat div_mul_eq_mul_div mul_div_assoc Filter.Tendsto.comp zero_div
completedHurwitzZetaEven₀_neg 📖	mathematical	—	completedHurwitzZetaEven₀ UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	hurwitzEvenFEPair_neg
completedHurwitzZetaEven₀_one_sub 📖	mathematical	—	completedHurwitzZetaEven₀ Complex Complex.instSub Complex.instOne completedCosZeta₀	—	completedHurwitzZetaEven₀.eq_1 completedCosZeta₀.eq_1 sub_div Nat.instAtLeastTwoHAddOfNat one_div Complex.ofReal_inv WeakFEPair.functional_equation₀ one_smul
continuousOn_cosKernel 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace cosKernel Set.Ioi Real.instPreorder Real.instZero	—	QuotientAddGroup.induction_on Continuous.comp_continuousOn Complex.continuous_re cosKernel_def continuousOn_of_forall_continuousAt ContinuousAt.comp continuousAt_jacobiTheta₂ MulZeroClass.mul_zero one_mul zero_add ContinuousAt.prodMk continuousAt_const ContinuousAt.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.continuousAt Complex.continuous_ofReal
continuousOn_evenKernel 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace evenKernel Set.Ioi Real.instPreorder Real.instZero	—	QuotientAddGroup.induction_on Continuous.comp_continuousOn Complex.continuous_re evenKernel_def continuousOn_of_forall_continuousAt ContinuousAt.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousAt.cexp ContinuousAt.fun_mul continuousAt_const Continuous.continuousAt Complex.continuous_ofReal ContinuousAt.comp continuousAt_jacobiTheta₂ MulZeroClass.mul_zero one_mul zero_add ContinuousAt.prodMk
cosKernel_def 📖	mathematical	—	Complex.ofReal cosKernel Real AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne jacobiTheta₂ Complex Complex.instMul Complex.I	—	Nat.instAtLeastTwoHAddOfNat cosKernel.eq_1 Complex.re_eq_add_conj jacobiTheta₂_conj Complex.conj_ofReal map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Complex.conj_I neg_mul neg_neg mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass two_ne_zero' CharZero.NeZero.two Complex.instCharZero
cosKernel_neg 📖	mathematical	—	cosKernel UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	QuotientAddGroup.induction_on cosKernel_def Complex.ofReal_neg jacobiTheta₂_neg_left
cosKernel_undef 📖	mathematical	Real Real.instLE Real.instZero	cosKernel	—	QuotientAddGroup.induction_on cosKernel_def jacobiTheta₂_undef MulZeroClass.mul_zero one_mul zero_add
cosZeta_apply_zero 📖	mathematical	—	cosZeta Complex Complex.instZero DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.instOne instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Function.update_self
cosZeta_neg 📖	mathematical	—	cosZeta UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	Function.update.congr_simp completedCosZeta_neg
cosZeta_neg_two_mul_nat_add_one 📖	mathematical	—	cosZeta Complex Complex.instMul Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instAdd Complex.instOne Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass neg_ne_zero two_ne_zero CharZero.NeZero.two Complex.instCharZero Nat.cast_add_one_ne_zero cosZeta.eq_1 Function.update_of_ne Complex.Gammaℝ_eq_zero_iff neg_mul Nat.cast_add_one div_zero
cosZeta_one_sub 📖	mathematical	—	cosZeta Complex Complex.instSub Complex.instOne Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instPow Complex.ofReal Real.pi Complex.instNeg Complex.Gamma Complex.cos DivInvMonoid.toDiv Complex.instDivInvMonoid hurwitzZetaEven	—	Nat.instAtLeastTwoHAddOfNat Complex.Gammaℂ.eq_1 cosZeta.eq_1 Function.update_of_ne CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero sub_zero div_eq_mul_inv completedCosZeta_one_sub Complex.inv_Gammaℝ_one_sub Nat.cast_add Nat.cast_one sub_add_cancel_right hurwitzZetaEven_def_of_ne_or_ne sub_self Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr 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 Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul 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.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf
differentiableAt_completedCosZeta 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField completedCosZeta	—	DifferentiableAt.div_const DifferentiableAt.comp WeakFEPair.differentiableAt_Λ div_ne_zero_iff two_ne_zero CharZero.NeZero.two Complex.instCharZero Nat.instAtLeastTwoHAddOfNat one_div Complex.ofReal_inv div_left_inj' NeZero.charZero_one differentiableAt_id
differentiableAt_completedHurwitzZetaEven 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField completedHurwitzZetaEven	—	DifferentiableAt.div_const DifferentiableAt.comp WeakFEPair.differentiableAt_Λ Complex.instCharZero one_div NeZero.charZero_one Nat.instAtLeastTwoHAddOfNat Complex.ofReal_div Complex.ofReal_one Complex.ofReal_ofNat div_left_inj' two_ne_zero CharZero.NeZero.two differentiableAt_id
differentiableAt_cosZeta 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField cosZeta	—	ne_or_eq differentiableAt_update_of_residue differentiableAt_completedCosZeta completedCosZeta_residue_zero DifferentiableAt.congr_of_eventuallyEq DifferentiableAt.fun_mul one_ne_zero NeZero.charZero_one Complex.instCharZero Differentiable.differentiableAt Complex.differentiable_Gammaℝ_inv Filter.mp_mem IsOpen.mem_nhds isOpen_compl_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Filter.univ_mem' cosZeta.eq_1 Function.update_of_ne div_eq_mul_inv
differentiableAt_hurwitzZetaEven 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField hurwitzZetaEven	—	Nat.instAtLeastTwoHAddOfNat differentiableAt_update_of_residue differentiableAt_completedHurwitzZetaEven completedHurwitzZetaEven_residue_zero MulZeroClass.zero_mul ite_mul div_eq_mul_inv
differentiableAt_hurwitzZetaEven_sub_one_div 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instSub hurwitzZetaEven DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.Gammaℝ	—	div_eq_mul_inv DifferentiableAt.mul completedHurwitzZetaEven_eq sub_sub add_assoc neg_sub div_neg neg_add_cancel add_zero DifferentiableAt.sub differentiable_completedHurwitzZetaEven₀ DifferentiableAt.div differentiableAt_const differentiableAt_id one_ne_zero NeZero.charZero_one Complex.instCharZero Differentiable.differentiableAt Complex.differentiable_Gammaℝ_inv DifferentiableAt.congr_of_eventuallyEq Filter.mp_mem eventually_ne_nhds T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Filter.univ_mem' hurwitzZetaEven.eq_1 Function.update_of_ne
differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instSub completedHurwitzZetaEven Complex.instOne	—	completedHurwitzZetaEven_eq sub_div Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg DifferentiableAt.sub differentiable_completedHurwitzZetaEven₀ DifferentiableAt.div differentiable_const differentiable_id one_ne_zero NeZero.charZero_one Complex.instCharZero
differentiableAt_update_of_residue 📖	mathematical	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.Tendsto Complex.instMul nhdsWithin Complex.instZero Compl.compl Set Set.instCompl Set.instSingletonSet nhds	Function.update Complex.instDecidableEq DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.Gammaℝ instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	DifferentiableAt.mul Differentiable.differentiableAt Complex.differentiable_Gammaℝ_inv Nat.instAtLeastTwoHAddOfNat Filter.Tendsto.congr' Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Pi.div_apply div_div mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Filter.Tendsto.div IsTopologicalDivisionRing.toContinuousInv₀ NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing Complex.Gammaℝ_residue_zero two_ne_zero CharZero.NeZero.two Complex.instCharZero ne_or_eq DifferentiableAt.congr_of_eventuallyEq IsOpen.mem_nhds isOpen_compl_singleton T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Function.update_of_ne Filter.Tendsto.limUnder_eq Complex.instT2Space PerfectSpace.not_isolated instPerfectSpace DifferentiableWithinAt.differentiableAt AddTorsor.nonempty Complex.differentiableOn_update_limUnder_of_isLittleO Complex.instCompleteSpace DifferentiableAt.differentiableWithinAt zero_div Complex.Gamma_zero MulZeroClass.mul_zero div_zero sub_zero Asymptotics.IsBigO.trans_isLittleO Asymptotics.isBigO_const_of_tendsto one_ne_zero' NeZero.charZero_one Asymptotics.isLittleO_iff_tendsto' Filter.eventually_of_mem inv_eq_zero Filter.Tendsto.congr one_div one_div_one_div nhdsWithin_le_nhds
differentiable_completedCosZeta₀ 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField completedCosZeta₀	—	Differentiable.div_const Differentiable.comp WeakFEPair.differentiable_Λ₀ differentiable_id
differentiable_completedHurwitzZetaEven₀ 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField completedHurwitzZetaEven₀	—	Differentiable.div_const Differentiable.comp WeakFEPair.differentiable_Λ₀ differentiable_id
differentiable_cosZeta_of_ne_zero 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField cosZeta	—	differentiableAt_cosZeta
differentiable_hurwitzZetaEven_sub_hurwitzZetaEven 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instSub hurwitzZetaEven	—	ne_or_eq DifferentiableAt.sub differentiableAt_hurwitzZetaEven Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg DifferentiableAt.fun_sub differentiableAt_hurwitzZetaEven_sub_one_div
evenKernel_def 📖	mathematical	—	Complex.ofReal evenKernel Real AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne Complex Complex.instMul Complex.exp Complex.instNeg Real.pi Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring jacobiTheta₂ Complex.I	—	neg_mul evenKernel.eq_1 Function.Periodic.lift.congr_simp Complex.ofReal_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_pow Nat.instAtLeastTwoHAddOfNat Complex.re_eq_add_conj jacobiTheta₂_conj map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Complex.conj_ofReal Complex.conj_I mul_neg neg_neg jacobiTheta₂_neg_left mul_div_cancel_right₀ EuclideanDomain.toMulDivCancelClass two_ne_zero' CharZero.NeZero.two Complex.instCharZero
evenKernel_eq_cosKernel_of_zero 📖	mathematical	—	evenKernel UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne cosKernel	—	evenKernel_def zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero MulZeroClass.zero_mul Complex.exp_zero one_mul cosKernel_def
evenKernel_functional_equation 📖	mathematical	—	evenKernel Real Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instPow instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat cosKernel	—	Nat.instAtLeastTwoHAddOfNat le_or_gt evenKernel_undef cosKernel_undef div_nonpos_of_nonneg_of_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing zero_le_one Real.instZeroLEOneClass MulZeroClass.mul_zero QuotientAddGroup.induction_on Complex.ofReal_mul evenKernel_def cosKernel_def jacobiTheta₂_functional_equation Complex.ofReal_div div_div mul_one_div Complex.div_I neg_one_mul neg_neg mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.I_ne_zero Complex.ofReal_ne_zero LT.lt.ne' div_eq_iff Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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 neg_mul mul_assoc Complex.I_mul_I Complex.ofReal_cpow LT.lt.le Complex.ofReal_one Complex.ofReal_ofNat mul_pow Complex.I_sq Mathlib.Tactic.Ring.neg_congr 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.mul_one Mathlib.Tactic.Ring.pow_congr 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_pow Mathlib.Tactic.Ring.pow_zero Nat.cast_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add mul_comm Complex.exp_add neg_add_cancel Complex.exp_zero mul_one
evenKernel_neg 📖	mathematical	—	evenKernel UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	QuotientAddGroup.induction_on evenKernel_def Complex.ofReal_neg Even.neg_pow Nat.instAtLeastTwoHAddOfNat neg_mul jacobiTheta₂_neg_left
evenKernel_undef 📖	mathematical	Real Real.instLE Real.instZero	evenKernel	—	QuotientAddGroup.induction_on evenKernel_def neg_mul jacobiTheta₂_undef MulZeroClass.mul_zero one_mul zero_add
hasSum_int_completedCosZeta 📖	mathematical	Real Real.instLT Real.instOne Complex.re	HasSum 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.instMul Complex.Gammaℝ Complex.exp instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Complex.instPow abs instLatticeInt Int.instAddGroup completedCosZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat HasSum.congr_fun HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_cosKernel₀ zero_div neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow div_mul_eq_mul_div mellin_div_const completedCosZeta.eq_1 WeakFEPair.hasMellin Complex.instCompleteSpace Complex.div_ofNat_re div_lt_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid hasSum_mellin_pi_mul_sq instCountableInt LT.lt.trans zero_lt_one Int.cast_eq_zero Summable.of_norm_bounded Real.instCompleteSpace Summable.div_const instIsTopologicalRingReal Real.summable_one_div_int_add_rpow Mathlib.Tactic.Ring.of_eq 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 norm_div Complex.norm_exp_ofReal_mul_I RCLike.norm_ofNat div_right_comm NormOneClass.norm_one NormedDivisionRing.to_normOneClass Real.norm_of_nonneg Real.rpow_nonneg abs_nonneg covariant_swap_add_of_covariant_add add_zero mul_div_assoc
hasSum_int_completedHurwitzZetaEven 📖	mathematical	Real Real.instLT Real.instOne Complex.re	HasSum 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.Gammaℝ Complex.instPow Complex.ofReal abs Real.lattice Real.instAddGroup Real.instAdd Real.instIntCast instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat completedHurwitzZetaEven AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat HasSum.congr_fun HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.hasSum_ofReal hasSum_int_evenKernel₀ Complex.ofReal_sub Complex.ofReal_zero zero_div mul_comm mul_one_div mellin_div_const WeakFEPair.hasMellin Complex.instCompleteSpace Complex.div_ofNat_re div_lt_div_iff_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid hasSum_mellin_pi_mul_sq instCountableInt LT.lt.trans zero_lt_one Summable.mul_left instIsTopologicalRingReal Real.summable_one_div_int_add_rpow div_right_comm
hasSum_int_cosKernel 📖	mathematical	Real Real.instLT Real.instZero	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 Complex.exp instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Real.exp Real.instMul Real.instNeg Monoid.toNatPow Real.instMonoid Real.instIntCast cosKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat cosKernel_def jacobiTheta₂_term.eq_1 Complex.exp_add Mathlib.Tactic.Ring.add_congr 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.Ring.neg_congr 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.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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add sub_eq_add_neg Complex.I_sq mul_neg neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow hasSum_jacobiTheta₂_term MulZeroClass.mul_zero one_mul zero_add
hasSum_int_cosKernel₀ 📖	mathematical	Real Real.instLT Real.instZero	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.instZero Complex.instMul Complex.exp instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Real.exp Real.instMul Real.instNeg Monoid.toNatPow Real.instMonoid Real.instIntCast Complex.instSub cosKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne Complex.instOne SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow Int.cast_zero MulZeroClass.mul_zero Complex.exp_zero zero_pow Nat.instCharZero MulZeroClass.zero_mul Real.exp_zero mul_one hasSum_ite_sub_hasSum SeminormedAddCommGroup.toIsTopologicalAddGroup SummationFilter.instLeAtTopUnconditional hasSum_int_cosKernel
hasSum_int_cosZeta 📖	mathematical	Real Real.instLT Real.instOne Complex.re	HasSum 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.exp Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Complex.instIntCast Complex.instPow abs instLatticeInt Int.instAddGroup cosZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat cosZeta.eq_1 Function.update_of_ne Complex.ne_zero_of_one_lt_re HasSum.congr_fun HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_completedCosZeta mul_div_assoc div_right_comm mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Complex.Gammaℝ_ne_zero_of_re_pos LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
hasSum_int_evenKernel 📖	mathematical	Real Real.instLT Real.instZero	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.exp Real.instMul Real.instNeg Real.pi Monoid.toNatPow Real.instMonoid Real.instAdd Real.instIntCast evenKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SummationFilter.unconditional	—	Complex.hasSum_ofReal evenKernel_def jacobiTheta₂_term.eq_1 Complex.exp_add Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one 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.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.mul_assoc_rev mul_one add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Meta.NormNum.instAtLeastTwo Complex.I_sq mul_neg neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow Complex.ofReal_add HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_jacobiTheta₂_term MulZeroClass.mul_zero one_mul zero_add
hasSum_int_evenKernel₀ 📖	mathematical	Real Real.instLT Real.instZero	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instAdd Real.instIntCast Real.decidableEq Real.exp Real.instMul Real.instNeg Real.pi Monoid.toNatPow Real.instMonoid Real.instSub evenKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne HasQuotient.Quotient AddSubgroup QuotientAddGroup.instHasQuotientAddSubgroup NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem AddSubgroup.decidableMemZMultiples Real.instAddGroup SummationFilter.unconditional	—	zsmul_one RCLike.charZero_rclike neg_mul Int.cast_neg neg_add_cancel zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.mul_zero MulZeroClass.zero_mul Real.exp_zero hasSum_ite_sub_hasSum instIsTopologicalAddGroupReal SummationFilter.instLeAtTopUnconditional hasSum_int_evenKernel Mathlib.Tactic.Contrapose.contrapose₂ Mathlib.Tactic.Push.not_forall_eq sub_zero
hasSum_int_hurwitzZetaEven 📖	mathematical	Real Real.instLT Real.instOne Complex.re	HasSum 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.instOne Complex.instPow Complex.ofReal abs Real.lattice Real.instAddGroup Real.instAdd Real.instIntCast instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat hurwitzZetaEven AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat hurwitzZetaEven.eq_1 Function.update_of_ne Complex.ne_zero_of_one_lt_re HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_completedHurwitzZetaEven HasSum.congr_fun div_right_comm div_self Complex.Gammaℝ_ne_zero_of_re_pos LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
hasSum_nat_completedCosZeta 📖	mathematical	Real Real.instLT Real.instOne Complex.re	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.instZero DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instMul Complex.Gammaℝ Complex.ofReal Real.cos Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.instPow Complex.instNatCast completedCosZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	abs_zero Int.instAddLeftMono Int.cast_zero Complex.zero_cpow Complex.ne_zero_of_one_lt_re Nat.instAtLeastTwoHAddOfNat HasSum.nat_add_neg IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_completedCosZeta HasSum.congr_fun add_zero zero_div div_zero Nat.cast_zero neg_zero zero_add Complex.ofReal_cos Complex.ofReal_mul Mathlib.Tactic.Ring.of_eq 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 neg_mul mul_div_assoc div_right_comm Int.cast_natCast Nat.abs_cast IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.cast_neg mul_neg abs_neg Distrib.leftDistribClass
hasSum_nat_cosKernel₀ 📖	mathematical	Real Real.instLT Real.instZero	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.cos Real.pi Real.instAdd Real.instOne Real.exp Real.instNeg Monoid.toNatPow Real.instMonoid Real.instSub cosKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Complex.hasSum_ofReal Complex.ofReal_sub Complex.ofReal_one HasSum.nat_add_neg IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_cosKernel HasSum.congr_fun mul_neg zero_sub sub_self add_sub_assoc Distrib.rightDistribClass neg_sq Int.cast_natCast Int.cast_neg mul_one Real.exp_zero Complex.exp_zero MulZeroClass.zero_mul MulZeroClass.mul_zero zero_pow two_ne_zero Int.cast_zero neg_zero Nat.cast_zero Finset.sum_range_one hasSum_nat_add_iff' SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.ofReal_mul Complex.ofReal_cos Complex.ofReal_add Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_pow Nat.cast_add Nat.cast_one Complex.cos.eq_1 mul_div_cancel₀ CharZero.NeZero.two Complex.instCharZero Mathlib.Tactic.Ring.of_eq 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.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr 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
hasSum_nat_cosZeta 📖	mathematical	Real Real.instLT Real.instOne Complex.re	HasSum 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.ofReal Real.cos Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.instPow Complex.instNatCast cosZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat HasSum.nat_add_neg IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_cosZeta Complex.ofReal_cos Complex.ofReal_mul neg_mul HasSum.congr_fun div_right_comm add_zero zero_div div_zero Complex.zero_cpow Complex.ne_zero_of_one_lt_re Int.cast_zero abs_zero Int.instAddLeftMono mul_neg Int.cast_natCast Nat.abs_cast IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.cast_neg abs_neg Mathlib.Tactic.Ring.of_eq 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
hasSum_nat_hurwitzZetaEven 📖	mathematical	Real Real.instLT Real.instOne Complex.re	HasSum 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.instAdd Complex.instOne Complex.instPow Complex.ofReal abs Real.lattice Real.instAddGroup Real.instAdd Real.instNatCast Real.instSub instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat hurwitzZetaEven AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	HasSum.congr_fun Nat.instAtLeastTwoHAddOfNat HasSum.nat_add_neg_add_one hasSum_int_hurwitzZetaEven one_div abs_neg neg_sub' neg_add_rev sub_neg_eq_add add_div Int.cast_natCast Int.cast_add Int.cast_neg Int.cast_one
hasSum_nat_hurwitzZetaEven_of_mem_Icc 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne Real.instLT Complex.re	HasSum 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.instAdd Complex.instOne Complex.instPow Complex.instNatCast Complex.ofReal Complex.instSub instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat hurwitzZetaEven AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	HasSum.congr_fun Nat.instAtLeastTwoHAddOfNat hasSum_nat_hurwitzZetaEven abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Real.instIsOrderedRing Mathlib.Tactic.Linarith.natCast_nonneg Mathlib.Tactic.Linarith.sub_neg_of_lt one_div Complex.ofReal_add Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Complex.ofReal_sub
hurwitzEvenFEPair_neg 📖	mathematical	—	hurwitzEvenFEPair UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	evenKernel_neg cosKernel_neg
hurwitzEvenFEPair_zero_symm 📖	mathematical	—	WeakFEPair.symm Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace hurwitzEvenFEPair UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	evenKernel_eq_cosKernel_of_zero inv_one WeakFEPair.hg_int WeakFEPair.hf_int WeakFEPair.hk WeakFEPair.h_feq' WeakFEPair.hg_top WeakFEPair.hf_top
hurwitzZetaEven_apply_zero 📖	mathematical	—	hurwitzZetaEven Complex Complex.instZero UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem AddSubgroup.decidableMemZMultiples Real.instAddGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.instOne instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Function.update_self
hurwitzZetaEven_def_of_ne_or_ne 📖	mathematical	—	hurwitzZetaEven Complex DivInvMonoid.toDiv Complex.instDivInvMonoid completedHurwitzZetaEven Complex.Gammaℝ	—	hurwitzZetaEven.eq_1 ne_or_eq Function.update_of_ne Function.update_self neg_zero zero_div Complex.cpow_zero Complex.Gamma_zero MulZeroClass.mul_zero div_zero NeZero.charZero_one Complex.instCharZero
hurwitzZetaEven_neg 📖	mathematical	—	hurwitzZetaEven UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne	—	Function.update.congr_simp completedHurwitzZetaEven_neg
hurwitzZetaEven_neg_two_mul_nat_add_one 📖	mathematical	—	hurwitzZetaEven Complex Complex.instMul Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instAdd Complex.instOne Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass neg_ne_zero two_ne_zero CharZero.NeZero.two Complex.instCharZero Nat.cast_add_one_ne_zero hurwitzZetaEven.eq_1 Function.update_of_ne Complex.Gammaℝ_eq_zero_iff neg_mul Nat.cast_add Nat.cast_one div_zero
hurwitzZetaEven_one_sub 📖	mathematical	—	hurwitzZetaEven Complex Complex.instSub Complex.instOne Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instPow Complex.ofReal Real.pi Complex.instNeg Complex.Gamma Complex.cos DivInvMonoid.toDiv Complex.instDivInvMonoid cosZeta	—	hurwitzZetaEven_def_of_ne_or_ne div_eq_mul_inv Nat.instAtLeastTwoHAddOfNat completedHurwitzZetaEven_one_sub Complex.inv_Gammaℝ_one_sub cosZeta.eq_1 Function.update_of_ne CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero neg_zero Complex.Gammaℂ.eq_1 Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.inv_congr 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 Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul 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.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf
hurwitzZetaEven_residue_one 📖	mathematical	—	Filter.Tendsto Complex Complex.instMul Complex.instSub Complex.instOne hurwitzZetaEven nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	Complex.Gammaℝ_one inv_one mul_one Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing completedHurwitzZetaEven_residue_one Filter.Tendsto.mono_left Continuous.tendsto Differentiable.continuous IsTopologicalSemiring.toContinuousAdd IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology Complex.differentiable_Gammaℝ_inv nhdsWithin_le_nhds Filter.Tendsto.congr' Filter.mp_mem eventually_ne_nhdsWithin T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace one_ne_zero NeZero.charZero_one Complex.instCharZero Filter.univ_mem' mul_div_assoc hurwitzZetaEven_def_of_ne_or_ne
isBigO_atTop_cosKernel_sub 📖	mathematical	—	Real Real.instLT Real.instZero Asymptotics.IsBigO Real.norm Filter.atTop Real.instPreorder Real.instSub cosKernel Real.instOne Real.exp Real.instMul Real.instNeg	—	QuotientAddGroup.induction_on HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub zero_le_one Real.instZeroLEOneClass Asymptotics.IsBigO.trans Nat.instAtLeastTwoHAddOfNat Filter.Eventually.isBigO Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_nat_cosKernel₀ eq_false_intro one_ne_zero NeZero.charZero_one RCLike.charZero_rclike sub_zero tsum_of_norm_bounded HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Summable.hasSum HurwitzKernelBounds.summable_f_nat norm_mul NormedDivisionRing.toNormMulClass Real.norm_two mul_assoc mul_le_mul_iff_of_pos_left IsOrderedRing.toPosMulMono PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing two_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.norm_of_nonneg LT.lt.le Real.exp_pos HurwitzKernelBounds.f_nat.eq_1 pow_zero one_mul Real.norm_eq_abs mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.abs_cos_le_one Asymptotics.IsBigO.const_mul_left
isBigO_atTop_evenKernel_sub 📖	mathematical	—	Real Real.instLT Real.instZero Asymptotics.IsBigO Real.norm Filter.atTop Real.instPreorder Real.instSub evenKernel UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem AddSubgroup.decidableMemZMultiples Real.instAddGroup Real.exp Real.instMul Real.instNeg	—	QuotientAddGroup.induction_on HurwitzKernelBounds.isBigO_atTop_F_int_zero_sub Asymptotics.IsBigO.trans Filter.EventuallyEq.isBigO Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_int_evenKernel neg_mul AddSubgroup.normal_of_comm Function.Periodic.lift.congr_simp pow_zero one_mul
tendsto_hurwitzZetaEven_sub_one_div_nhds_one 📖	mathematical	—	Filter.Tendsto Complex Complex.instSub hurwitzZetaEven DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.Gammaℝ nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	one_div sub_self div_zero Complex.Gammaℝ_one div_one sub_zero ContinuousAt.tendsto DifferentiableAt.continuousAt IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology differentiableAt_hurwitzZetaEven_sub_one_div

---

← Back to Index