HurwitzZetaOdd

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

Statistics

Metric	Count
Definitions completedHurwitzZetaOdd, completedSinZeta, hurwitzOddFEPair, hurwitzZetaOdd, jacobiTheta₂'', oddKernel, sinKernel, sinZeta	8
Theorems LSeriesHasSum_sin, completedHurwitzZetaOdd_neg, completedHurwitzZetaOdd_one_sub, completedSinZeta_neg, completedSinZeta_one_sub, continuousOn_oddKernel, continuousOn_sinKernel, differentiableAt_sinZeta, differentiable_completedHurwitzZetaOdd, differentiable_completedSinZeta, differentiable_hurwitzZetaOdd, hasSum_int_completedHurwitzZetaOdd, hasSum_int_completedSinZeta, hasSum_int_hurwitzZetaOdd, hasSum_int_oddKernel, hasSum_int_sinKernel, hasSum_int_sinZeta, hasSum_nat_completedSinZeta, hasSum_nat_hurwitzZetaOdd, hasSum_nat_hurwitzZetaOdd_of_mem_Icc, hasSum_nat_sinKernel, hasSum_nat_sinZeta, hurwitzOddFEPair_f, hurwitzOddFEPair_f₀, hurwitzOddFEPair_g, hurwitzOddFEPair_g₀, hurwitzOddFEPair_k, hurwitzOddFEPair_ε, hurwitzZetaOdd_neg, hurwitzZetaOdd_neg_two_mul_nat_sub_one, hurwitzZetaOdd_one_sub, isBigO_atTop_oddKernel, isBigO_atTop_sinKernel, jacobiTheta₂''_add_left, jacobiTheta₂''_conj, jacobiTheta₂''_neg_left, jacobiTheta₂'_functional_equation', oddKernel_def, oddKernel_def', oddKernel_functional_equation, oddKernel_neg, oddKernel_undef, oddKernel_zero, sinKernel_def, sinKernel_neg, sinKernel_undef, sinKernel_zero, sinZeta_neg, sinZeta_neg_two_mul_nat_sub_one, sinZeta_one_sub	50
Total	58

HurwitzZeta

Definitions

Name	Category	Theorems
completedHurwitzZetaOdd 📖	CompOp	6 math math: ZMod.completedLFunction_def_odd, hasSum_int_completedHurwitzZetaOdd, completedSinZeta_one_sub, completedHurwitzZetaOdd_neg, completedHurwitzZetaOdd_one_sub, differentiable_completedHurwitzZetaOdd
completedSinZeta 📖	CompOp	6 math math: completedSinZeta_neg, completedSinZeta_one_sub, hasSum_nat_completedSinZeta, completedHurwitzZetaOdd_one_sub, hasSum_int_completedSinZeta, differentiable_completedSinZeta
hurwitzOddFEPair 📖	CompOp	6 math math: hurwitzOddFEPair_f₀, hurwitzOddFEPair_ε, hurwitzOddFEPair_g₀, hurwitzOddFEPair_f, hurwitzOddFEPair_k, hurwitzOddFEPair_g
hurwitzZetaOdd 📖	CompOp	11 math math: hasSum_int_hurwitzZetaOdd, ZMod.LFunction_def_odd, differentiable_hurwitzZetaOdd, hurwitzZetaOdd_neg_two_mul_nat, hasSum_nat_hurwitzZetaOdd, hurwitzZetaOdd_eq, hurwitzZetaOdd_neg_two_mul_nat_sub_one, hurwitzZetaOdd_neg, hurwitzZetaOdd_one_sub, hasSum_nat_hurwitzZetaOdd_of_mem_Icc, sinZeta_one_sub
jacobiTheta₂'' 📖	CompOp	5 math math: jacobiTheta₂''_neg_left, jacobiTheta₂''_add_left, jacobiTheta₂'_functional_equation', oddKernel_def, jacobiTheta₂''_conj
oddKernel 📖	CompOp	10 math math: oddKernel_def', oddKernel_def, continuousOn_oddKernel, oddKernel_zero, oddKernel_functional_equation, isBigO_atTop_oddKernel, oddKernel_neg, hasSum_int_oddKernel, hurwitzOddFEPair_f, oddKernel_undef
sinKernel 📖	CompOp	10 math math: sinKernel_neg, hasSum_nat_sinKernel, continuousOn_sinKernel, sinKernel_zero, hasSum_int_sinKernel, oddKernel_functional_equation, sinKernel_undef, sinKernel_def, hurwitzOddFEPair_g, isBigO_atTop_sinKernel
sinZeta 📖	CompOp	11 math math: sinZeta_neg_two_mul_nat_sub_one, hasSum_nat_sinZeta, sinZeta_two_mul_nat_add_one', sinZeta_two_mul_nat_add_one, sinZeta_neg, hasSum_int_sinZeta, LSeriesHasSum_sin, sinZeta_eq, hurwitzZetaOdd_one_sub, sinZeta_one_sub, differentiableAt_sinZeta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LSeriesHasSum_sin 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeriesHasSum Complex.ofReal Real.sin Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi sinZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples	—	HasSum.congr_fun Nat.instAtLeastTwoHAddOfNat hasSum_nat_sinZeta LSeries.term_of_ne_zero' Complex.ne_zero_of_one_lt_re
completedHurwitzZetaOdd_neg 📖	mathematical	—	completedHurwitzZetaOdd UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Complex Complex.instNeg	—	oddKernel_neg Complex.ofReal_neg mul_neg MeasureTheory.integral_neg neg_div
completedHurwitzZetaOdd_one_sub 📖	mathematical	—	completedHurwitzZetaOdd Complex Complex.instSub Complex.instOne completedSinZeta	—	completedHurwitzZetaOdd.eq_1 completedSinZeta.eq_1 Nat.instAtLeastTwoHAddOfNat Complex.ofReal_div Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.mul_pf_left 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.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_add Mathlib.Meta.NormNum.IsRat.of_raw Mathlib.Meta.NormNum.IsRat.den_nz hurwitzOddFEPair_k StrongFEPair.functional_equation hurwitzOddFEPair_ε one_smul
completedSinZeta_neg 📖	mathematical	—	completedSinZeta UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Complex Complex.instNeg	—	WeakFEPair.hg_int WeakFEPair.hf_int WeakFEPair.hk inv_one WeakFEPair.h_feq' WeakFEPair.hg_top WeakFEPair.hf_top StrongFEPair.hg₀ StrongFEPair.hf₀ sinKernel_neg Complex.ofReal_neg mul_neg MeasureTheory.integral_neg neg_div
completedSinZeta_one_sub 📖	mathematical	—	completedSinZeta Complex Complex.instSub Complex.instOne completedHurwitzZetaOdd	—	sub_sub_cancel
continuousOn_oddKernel 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace oddKernel Set.Ioi Real.instPreorder Real.instZero	—	QuotientAddGroup.induction_on Nat.instAtLeastTwoHAddOfNat oddKernel_def' ContinuousAt.continuousWithinAt ContinuousAt.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Continuous.continuousAt Continuous.cexp Continuous.comp' Continuous.fun_mul continuous_const continuous_id' Complex.continuous_ofReal Continuous.prodMk ContinuousAt.add IsTopologicalSemiring.toContinuousAdd ContinuousAt.div_const ContinuousAt.comp continuousAt_jacobiTheta₂' Complex.I_mul_im Complex.ofReal_re continuousAt_const continuousAt_jacobiTheta₂ ContinuousOn.congr Continuous.comp_continuousOn Complex.continuous_re
continuousOn_sinKernel 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace sinKernel Set.Ioi Real.instPreorder Real.instZero	—	QuotientAddGroup.induction_on Nat.instAtLeastTwoHAddOfNat sinKernel_def ContinuousOn.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuousOn_of_forall_continuousAt continuousAt_jacobiTheta₂' Complex.I_mul_im Complex.ofReal_re ContinuousAt.comp' ContinuousAt.prodMk continuousAt_const ContinuousAt.fun_mul Continuous.continuousAt Complex.continuous_ofReal ContinuousOn.congr Continuous.comp_continuousOn Complex.continuous_re
differentiableAt_sinZeta 📖	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 sinZeta	—	Differentiable.mul differentiable_completedSinZeta Differentiable.comp Complex.differentiable_Gammaℝ_inv Differentiable.add differentiable_id differentiable_const
differentiable_completedHurwitzZetaOdd 📖	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 completedHurwitzZetaOdd	—	Differentiable.div_const Differentiable.comp StrongFEPair.differentiable_Λ Differentiable.add_const differentiable_id Nat.instAtLeastTwoHAddOfNat
differentiable_completedSinZeta 📖	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 completedSinZeta	—	Differentiable.div_const Differentiable.comp StrongFEPair.differentiable_Λ Differentiable.add_const differentiable_id Nat.instAtLeastTwoHAddOfNat
differentiable_hurwitzZetaOdd 📖	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 hurwitzZetaOdd	—	Differentiable.mul differentiable_completedHurwitzZetaOdd Differentiable.comp Complex.differentiable_Gammaℝ_inv Differentiable.add differentiable_id differentiable_const
hasSum_int_completedHurwitzZetaOdd 📖	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.instAdd Complex.instOne SignType.cast Complex.instZero Complex.instNeg DFunLike.coe OrderHom SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT Real.instAdd Real.instIntCast Complex.instPow Complex.ofReal abs Real.lattice Real.instAddGroup instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat completedHurwitzZetaOdd 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_oddKernel Complex.ofReal_add div_mul_eq_mul_div one_mul neg_mul Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_mul Complex.ofReal_pow mul_one_div Summable.mul_left instIsTopologicalRingReal Real.summable_one_div_int_add_rpow hasSum_mellin_pi_mul_sq' instCountableInt LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike mellin_div_const div_right_comm
hasSum_int_completedSinZeta 📖	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.instAdd Complex.instOne Complex.instNeg Complex.I Complex.instIntCast Complex.exp instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.instPow abs instLatticeInt Int.instAddGroup completedSinZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat 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 norm_div RCLike.norm_ofNat norm_mul NormedDivisionRing.toNormMulClass norm_neg Complex.norm_I one_mul Complex.norm_exp_ofReal_mul_I HasSum.congr_fun HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_sinKernel div_mul_eq_mul_div mul_right_comm div_right_comm Summable.div_const instIsTopologicalRingReal Summable.of_nat_of_neg instIsTopologicalAddGroupReal Int.cast_natCast Nat.abs_cast Real.instIsOrderedRing one_div Int.cast_neg abs_neg hasSum_mellin_pi_mul_sq' instCountableInt LT.lt.trans zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike mellin_div_const mul_neg Int.sign_eq_sign SignType.intCast_cast neg_mul sign_intCast Real.instNontrivial Real.instIsStrictOrderedRing Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.one_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.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
hasSum_int_hurwitzZetaOdd 📖	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 SignType.cast Complex.instZero Complex.instOne Complex.instNeg DFunLike.coe OrderHom SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT Real.instAdd Real.instIntCast Complex.instPow Complex.ofReal abs Real.lattice Real.instAddGroup instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat hurwitzZetaOdd AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	HasSum.congr_fun Nat.instAtLeastTwoHAddOfNat HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_completedHurwitzZetaOdd Complex.add_re Complex.one_re add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one div_right_comm mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Complex.Gammaℝ_ne_zero_of_re_pos
hasSum_int_oddKernel 📖	mathematical	Real Real.instLT Real.instZero	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Real.instAdd Real.instIntCast Real.exp Real.instNeg Real.pi Monoid.toNatPow Real.instMonoid oddKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SummationFilter.unconditional	—	Complex.hasSum_ofReal Nat.instAtLeastTwoHAddOfNat oddKernel_def' hasSum_jacobiTheta₂_term Complex.I_mul_im Complex.ofReal_re hasSum_jacobiTheta₂'_term HasSum.congr_fun HasSum.mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasSum.add IsTopologicalSemiring.toContinuousAdd HasSum.div_const jacobiTheta₂'_term.eq_1 mul_assoc mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Complex.two_pi_I_ne_zero add_mul Distrib.rightDistribClass mul_left_comm jacobiTheta₂_term.eq_1 Complex.exp_add Complex.ofReal_mul Complex.ofReal_add Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_pow mul_right_comm Complex.I_mul_I Mathlib.Tactic.Ring.mul_congr 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.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero 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.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.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 Nat.cast_one
hasSum_int_sinKernel 📖	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.instNeg Complex.I Complex.instIntCast Complex.exp instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Real.exp Real.instMul Real.instNeg Monoid.toNatPow Real.instMonoid Real.instIntCast sinKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat neg_mul NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero sinKernel_def HasSum.congr_fun HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_jacobiTheta₂'_term Complex.I_mul_im Complex.ofReal_re jacobiTheta₂'_term.eq_1 jacobiTheta₂_term.eq_1 Complex.ofReal_exp mul_assoc Complex.exp_add eq_div_iff Complex.ofReal_mul Complex.ofReal_pow Complex.ofReal_neg Complex.ofReal_intCast mul_comm mul_neg neg_neg mul_right_comm Complex.I_mul_I one_mul
hasSum_int_sinZeta 📖	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.instNeg Complex.I Complex.instIntCast Complex.exp instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.instPow abs instLatticeInt Int.instAddGroup sinZeta AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat sinZeta.eq_1 HasSum.congr_fun HasSum.div_const IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_completedSinZeta Complex.add_re Complex.one_re add_pos' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid lt_trans Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one mul_assoc div_right_comm mul_div_cancel_left₀ EuclideanDomain.toMulDivCancelClass Complex.Gammaℝ_ne_zero_of_re_pos
hasSum_nat_completedSinZeta 📖	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.instAdd Complex.instOne Complex.ofReal Real.sin Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.instPow Complex.instNatCast completedSinZeta 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_completedSinZeta HasSum.congr_fun Int.cast_natCast Int.cast_neg Nat.abs_cast IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing abs_neg add_zero zero_div MulZeroClass.zero_mul MulZeroClass.mul_zero Int.cast_zero div_right_comm eq_or_ne CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike Real.sin_zero Complex.instCharZero mul_neg Int.instCharZero Complex.exp_zero mul_one neg_zero Int.cast_one Complex.ofReal_sin Complex.ofReal_mul mul_assoc Distrib.leftDistribClass mul_neg_one neg_neg neg_mul sub_eq_neg_add mul_sub mul_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_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_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_hurwitzZetaOdd 📖	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.instSub SignType.cast Complex.instZero Complex.instOne Complex.instNeg DFunLike.coe OrderHom SignType Real.instPreorder PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder SignType.instLinearOrder OrderHom.instFunLike SignType.sign Real.instZero Real.decidableLT Real.instAdd Real.instNatCast Complex.instPow Complex.ofReal abs Real.lattice Real.instAddGroup Real.instSub instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat hurwitzZetaOdd AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	HasSum.congr_fun Nat.instAtLeastTwoHAddOfNat HasSum.nat_add_neg_add_one hasSum_int_hurwitzZetaOdd Int.cast_neg Int.cast_add Int.cast_one sub_div sub_eq_add_neg Int.cast_natCast Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero 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_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_neg mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Left.sign_neg IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid abs_neg SignType.coe_neg neg_div
hasSum_nat_hurwitzZetaOdd_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.instSub Complex.instOne Complex.instPow Complex.instAdd Complex.instNatCast Complex.ofReal instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat hurwitzZetaOdd AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples SummationFilter.unconditional	—	HasSum.congr_fun Nat.instAtLeastTwoHAddOfNat hasSum_nat_hurwitzZetaOdd abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid add_nonneg Nat.cast_nonneg' Real.instZeroLEOneClass Complex.ofReal_add lt_or_eq_of_le sign_pos one_div Complex.ofReal_zero Complex.zero_cpow not_lt zero_le_one Complex.zero_re div_zero add_sub_assoc sub_nonneg covariant_swap_add_of_covariant_add Complex.ofReal_sub
hasSum_nat_sinKernel 📖	mathematical	Real Real.instLT Real.instZero	HasSum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.sin Real.pi Real.exp Real.instNeg Monoid.toNatPow Real.instMonoid sinKernel AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat Complex.hasSum_ofReal HasSum.nat_add_neg IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasSum_int_sinKernel HasSum.congr_fun Int.cast_zero MulZeroClass.mul_zero MulZeroClass.zero_mul add_zero Int.cast_neg neg_sq mul_neg Complex.ofReal_mul Int.cast_natCast Distrib.rightDistribClass Complex.ofReal_sin Complex.ofReal_exp Complex.ofReal_neg Complex.ofReal_pow mul_div_assoc div_mul_eq_mul_div div_self two_ne_zero CharZero.NeZero.two Complex.instCharZero one_mul neg_mul neg_neg mul_comm mul_assoc sub_eq_neg_add mul_sub Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_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_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_sinZeta 📖	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.sin Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Complex.instPow Complex.instNatCast sinZeta 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_sinZeta Complex.ofReal_sin Complex.ofReal_mul HasSum.congr_fun 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 ne_or_eq neg_mul sub_mul div_right_comm Int.cast_one mul_one mul_comm neg_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_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_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 CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero MulZeroClass.mul_zero neg_zero MulZeroClass.zero_mul Complex.exp_zero sub_self Int.instCharZero
hurwitzOddFEPair_f 📖	mathematical	—	WeakFEPair.f Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace StrongFEPair.toWeakFEPair hurwitzOddFEPair Real Complex.ofReal oddKernel	—	—
hurwitzOddFEPair_f₀ 📖	mathematical	—	WeakFEPair.f₀ Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace StrongFEPair.toWeakFEPair hurwitzOddFEPair Complex.instZero	—	—
hurwitzOddFEPair_g 📖	mathematical	—	WeakFEPair.g Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace StrongFEPair.toWeakFEPair hurwitzOddFEPair Real Complex.ofReal sinKernel	—	—
hurwitzOddFEPair_g₀ 📖	mathematical	—	WeakFEPair.g₀ Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace StrongFEPair.toWeakFEPair hurwitzOddFEPair Complex.instZero	—	—
hurwitzOddFEPair_k 📖	mathematical	—	WeakFEPair.k Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace StrongFEPair.toWeakFEPair hurwitzOddFEPair Real DivInvMonoid.toDiv Real.instDivInvMonoid instOfNatAtLeastTwo Real.instNatCast	—	—
hurwitzOddFEPair_ε 📖	mathematical	—	WeakFEPair.ε Complex Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace StrongFEPair.toWeakFEPair hurwitzOddFEPair Complex.instOne	—	—
hurwitzZetaOdd_neg 📖	mathematical	—	hurwitzZetaOdd UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Complex Complex.instNeg	—	completedHurwitzZetaOdd_neg neg_div
hurwitzZetaOdd_neg_two_mul_nat_sub_one 📖	mathematical	—	hurwitzZetaOdd Complex Complex.instSub Complex.instMul Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instOne Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat hurwitzZetaOdd.eq_1 Complex.Gammaℝ_eq_zero_iff neg_mul sub_add_cancel div_zero
hurwitzZetaOdd_one_sub 📖	mathematical	—	hurwitzZetaOdd Complex Complex.instSub Complex.instOne Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instPow Complex.ofReal Real.pi Complex.instNeg Complex.Gamma Complex.sin DivInvMonoid.toDiv Complex.instDivInvMonoid sinZeta	—	Nat.instAtLeastTwoHAddOfNat Complex.Gammaℂ.eq_1 hurwitzZetaOdd.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.instAtLeastTwo div_eq_mul_inv Complex.inv_Gammaℝ_two_sub completedHurwitzZetaOdd_one_sub sinZeta.eq_1 mul_div_assoc mul_comm
isBigO_atTop_oddKernel 📖	mathematical	—	Real Real.instLT Real.instZero Asymptotics.IsBigO Real.norm Filter.atTop Real.instPreorder oddKernel Real.exp Real.instMul Real.instNeg	—	QuotientAddGroup.induction_on HurwitzKernelBounds.isBigO_atTop_F_int_one Asymptotics.IsBigO.trans 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_int_oddKernel neg_mul Function.Periodic.lift.congr_simp pow_one norm_mul NormedDivisionRing.toNormMulClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid LT.lt.le Real.exp_pos norm_tsum_le_tsum_norm Summable.norm FiniteDimensional.rclike_to_real HasSum.summable
isBigO_atTop_sinKernel 📖	mathematical	—	Real Real.instLT Real.instZero Asymptotics.IsBigO Real.norm Filter.atTop Real.instPreorder sinKernel Real.exp Real.instMul Real.instNeg	—	QuotientAddGroup.induction_on HurwitzKernelBounds.isBigO_atTop_F_nat_one le_refl Asymptotics.IsBigO.trans Nat.instAtLeastTwoHAddOfNat Filter.Eventually.isBigO Filter.mp_mem Filter.eventually_gt_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial Filter.univ_mem' HurwitzKernelBounds.F_nat.eq_1 HasSum.tsum_eq TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace SummationFilter.instNeBotUnconditional hasSum_nat_sinKernel 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 Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid HurwitzKernelBounds.f_nat.eq_1 pow_one add_zero Real.norm_of_nonneg LT.lt.le Real.exp_pos Real.norm_eq_abs Nat.abs_cast mul_le_mul_iff_of_pos_right IsOrderedRing.toMulPosMono MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono mul_le_of_le_one_right Nat.cast_nonneg Real.abs_sin_le_one Asymptotics.IsBigO.const_mul_left
jacobiTheta₂''_add_left 📖	mathematical	—	jacobiTheta₂'' Complex Complex.instAdd Complex.instOne	—	Nat.instAtLeastTwoHAddOfNat add_mul Distrib.rightDistribClass one_mul jacobiTheta₂'_add_left' jacobiTheta₂_add_left' div_add' Complex.two_pi_I_ne_zero mul_left_comm mul_add Distrib.leftDistribClass mul_assoc Complex.exp_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr 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 Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_gt 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_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_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.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_one 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.Tactic.Ring.neg_zero Mathlib.Meta.NormNum.instAtLeastTwo 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.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf
jacobiTheta₂''_conj 📖	mathematical	—	DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing jacobiTheta₂'' Complex.instNeg	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Complex.conj_ofReal Complex.conj_I mul_neg map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass neg_mul map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat map_div₀ jacobiTheta₂'_conj map_ofNat div_neg jacobiTheta₂_conj jacobiTheta₂'_neg_left neg_div jacobiTheta₂_neg_left
jacobiTheta₂''_neg_left 📖	mathematical	—	jacobiTheta₂'' Complex Complex.instNeg	—	Even.neg_pow Nat.instAtLeastTwoHAddOfNat neg_mul jacobiTheta₂'_neg_left neg_div jacobiTheta₂_neg_left mul_neg
jacobiTheta₂'_functional_equation' 📖	mathematical	—	jacobiTheta₂' Complex Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.instPow Complex.I jacobiTheta₂'' Complex.instOne	—	Nat.instAtLeastTwoHAddOfNat eq_or_ne jacobiTheta₂'_undef MulZeroClass.mul_zero Complex.zero_cpow Complex.instCharZero div_zero MulZeroClass.zero_mul div_eq_iff Complex.two_pi_I_ne_zero mul_comm mul_assoc Complex.I_mul_I neg_mul mul_neg mul_one jacobiTheta₂'_functional_equation mul_one_div mul_right_comm Complex.cpow_one div_div div_self neg_ne_zero Complex.I_ne_zero div_mul_div_comm Complex.cpow_add mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass div_mul_eq_mul_div Mathlib.Meta.NormNum.isNNRat_eq_true Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.instAtLeastTwo jacobiTheta₂''.eq_1 div_add' mul_div_assoc mul_div mul_neg_one neg_div jacobiTheta₂_neg_left jacobiTheta₂'_neg_left neg_sub sub_eq_neg_add
oddKernel_def 📖	mathematical	—	Complex.ofReal oddKernel Real AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne jacobiTheta₂'' Complex Complex.instMul Complex.I	—	oddKernel.eq_1 jacobiTheta₂''_conj Complex.conj_ofReal map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Complex.conj_I neg_mul neg_neg
oddKernel_def' 📖	mathematical	—	Complex.ofReal oddKernel 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 Complex.instAdd DivInvMonoid.toDiv Complex.instDivInvMonoid jacobiTheta₂' Complex.I instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat jacobiTheta₂	—	Nat.instAtLeastTwoHAddOfNat oddKernel_def jacobiTheta₂''.eq_1 mul_assoc 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 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 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 Complex.I_sq neg_one_mul
oddKernel_functional_equation 📖	mathematical	—	oddKernel Real Real.instMul DivInvMonoid.toDiv Real.instDivInvMonoid Real.instOne Real.instPow instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat sinKernel	—	Nat.instAtLeastTwoHAddOfNat le_or_gt oddKernel_undef sinKernel_undef one_div_nonpos IsOrderedRing.toPosMulMono Real.instIsOrderedRing MulZeroClass.mul_zero QuotientAddGroup.induction_on one_div Complex.ofReal_inv mul_comm div_div div_inv_eq_mul div_eq_mul_inv Complex.inv_I mul_neg neg_one_mul neg_mul neg_neg mul_assoc Complex.I_mul_I one_mul Complex.ofReal_div Complex.ofReal_one LT.lt.ne' Complex.arg_ofReal_of_nonneg LT.lt.le Real.pi_ne_zero oddKernel_def Complex.ofReal_mul sinKernel_def jacobiTheta₂'_functional_equation' Complex.inv_cpow Complex.ofReal_cpow Complex.ofReal_ofNat mul_div_assoc eq_div_iff mul_ne_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass neg_ne_zero two_ne_zero CharZero.NeZero.two Complex.instCharZero Complex.ofReal_ne_zero div_eq_inv_mul mul_right_comm
oddKernel_neg 📖	mathematical	—	oddKernel UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Real.instNeg	—	QuotientAddGroup.induction_on oddKernel_def Complex.ofReal_neg jacobiTheta₂''_neg_left
oddKernel_undef 📖	mathematical	Real Real.instLE Real.instZero	oddKernel	—	QuotientAddGroup.induction_on Complex.ofReal_eq_zero Nat.instAtLeastTwoHAddOfNat oddKernel_def' jacobiTheta₂_undef MulZeroClass.mul_zero one_mul zero_add jacobiTheta₂'_undef zero_div
oddKernel_zero 📖	mathematical	—	oddKernel UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Real.instZero	—	neg_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike oddKernel_neg
sinKernel_def 📖	mathematical	—	Complex.ofReal sinKernel Real AddCommGroup.toAddGroup Real.instAddCommGroup AddSubgroup.zmultiples Real.instOne Complex DivInvMonoid.toDiv Complex.instDivInvMonoid jacobiTheta₂' Complex.instMul Complex.I Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi	—	Nat.instAtLeastTwoHAddOfNat neg_mul sinKernel.eq_1 Function.Periodic.lift.congr_simp Complex.re_eq_add_conj map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass jacobiTheta₂'_conj Complex.conj_ofReal map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass Complex.conj_I neg_neg map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass Complex.instCharZero SemilinearMapClass.distribMulActionSemiHomClass RingHomClass.toLinearMapClassNNRat map_ofNat add_self_div_two CharZero.NeZero.two
sinKernel_neg 📖	mathematical	—	sinKernel UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Real.instNeg	—	QuotientAddGroup.induction_on Nat.instAtLeastTwoHAddOfNat sinKernel_def Complex.ofReal_neg jacobiTheta₂'_neg_left neg_mul neg_div
sinKernel_undef 📖	mathematical	Real Real.instLE Real.instZero	sinKernel	—	QuotientAddGroup.induction_on Complex.ofReal_eq_zero Nat.instAtLeastTwoHAddOfNat sinKernel_def jacobiTheta₂'_undef MulZeroClass.mul_zero one_mul zero_add zero_div
sinKernel_zero 📖	mathematical	—	sinKernel UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Real.instZero	—	neg_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass RCLike.charZero_rclike sinKernel_neg
sinZeta_neg 📖	mathematical	—	sinZeta UnitAddCircle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne Complex Complex.instNeg	—	completedSinZeta_neg neg_div
sinZeta_neg_two_mul_nat_sub_one 📖	mathematical	—	sinZeta Complex Complex.instSub Complex.instMul Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instOne Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat sinZeta.eq_1 Complex.Gammaℝ_eq_zero_iff neg_mul sub_add_cancel div_zero
sinZeta_one_sub 📖	mathematical	—	sinZeta Complex Complex.instSub Complex.instOne Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instPow Complex.ofReal Real.pi Complex.instNeg Complex.Gamma Complex.sin DivInvMonoid.toDiv Complex.instDivInvMonoid hurwitzZetaOdd	—	Nat.instAtLeastTwoHAddOfNat Complex.Gammaℂ.eq_1 sinZeta.eq_1 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one 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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.instAtLeastTwo div_eq_mul_inv Complex.inv_Gammaℝ_two_sub completedSinZeta_one_sub hurwitzZetaOdd.eq_1 mul_div_assoc mul_comm

---

← Back to Index