TwoVariable

📁 Source: Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean

Statistics

Metric	Count
Definitions jacobiTheta₂, jacobiTheta₂', jacobiTheta₂'_term, jacobiTheta₂_fderiv, jacobiTheta₂_term, jacobiTheta₂_term_fderiv	6
Theorems continuousAt_jacobiTheta₂, continuousAt_jacobiTheta₂', differentiableAt_jacobiTheta₂_fst, differentiableAt_jacobiTheta₂_snd, hasDerivAt_jacobiTheta₂_fst, hasFDerivAt_jacobiTheta₂, hasFDerivAt_jacobiTheta₂_term, hasSum_jacobiTheta₂'_term, hasSum_jacobiTheta₂_term, hasSum_jacobiTheta₂_term_fderiv, jacobiTheta₂'_add_left, jacobiTheta₂'_add_left', jacobiTheta₂'_add_right, jacobiTheta₂'_conj, jacobiTheta₂'_functional_equation, jacobiTheta₂'_neg_left, jacobiTheta₂'_undef, jacobiTheta₂_add_left, jacobiTheta₂_add_left', jacobiTheta₂_add_right, jacobiTheta₂_conj, jacobiTheta₂_fderiv_undef, jacobiTheta₂_functional_equation, jacobiTheta₂_neg_left, jacobiTheta₂_undef, norm_jacobiTheta₂'_term_le, norm_jacobiTheta₂_term, norm_jacobiTheta₂_term_fderiv_ge, norm_jacobiTheta₂_term_fderiv_le, norm_jacobiTheta₂_term_le, summable_jacobiTheta₂'_term_iff, summable_jacobiTheta₂_term_fderiv_iff, summable_jacobiTheta₂_term_iff, summable_pow_mul_jacobiTheta₂_term_bound	34
Total	40

(root)

Definitions

Name	Category	Theorems
jacobiTheta₂ 📖	CompOp	19 math math: jacobiTheta₂_conj, jacobiTheta₂_functional_equation, HurwitzZeta.evenKernel_def, HurwitzZeta.oddKernel_def', jacobiTheta₂_neg_left, hasSum_jacobiTheta₂_term, hasDerivAt_jacobiTheta₂_fst, differentiableAt_jacobiTheta₂_fst, jacobiTheta₂'_add_left', jacobiTheta₂'_functional_equation, hasFDerivAt_jacobiTheta₂, jacobiTheta₂_undef, HurwitzZeta.cosKernel_def, continuousAt_jacobiTheta₂, differentiableAt_jacobiTheta₂_snd, jacobiTheta_eq_jacobiTheta₂, jacobiTheta₂_add_left, jacobiTheta₂_add_left', jacobiTheta₂_add_right
jacobiTheta₂' 📖	CompOp	13 math math: HurwitzZeta.jacobiTheta₂'_functional_equation', jacobiTheta₂'_conj, HurwitzZeta.oddKernel_def', hasDerivAt_jacobiTheta₂_fst, hasSum_jacobiTheta₂'_term, jacobiTheta₂'_add_right, jacobiTheta₂'_neg_left, jacobiTheta₂'_add_left', jacobiTheta₂'_functional_equation, jacobiTheta₂'_undef, continuousAt_jacobiTheta₂', HurwitzZeta.sinKernel_def, jacobiTheta₂'_add_left
jacobiTheta₂'_term 📖	CompOp	3 math math: hasSum_jacobiTheta₂'_term, norm_jacobiTheta₂'_term_le, summable_jacobiTheta₂'_term_iff
jacobiTheta₂_fderiv 📖	CompOp	3 math math: hasSum_jacobiTheta₂_term_fderiv, hasFDerivAt_jacobiTheta₂, jacobiTheta₂_fderiv_undef
jacobiTheta₂_term 📖	CompOp	7 math math: norm_jacobiTheta₂_term_le, norm_jacobiTheta₂_term_fderiv_ge, hasSum_jacobiTheta₂_term, hasFDerivAt_jacobiTheta₂_term, norm_jacobiTheta₂_term, summable_jacobiTheta₂_term_iff, norm_jacobiTheta₂_term_fderiv_le
jacobiTheta₂_term_fderiv 📖	CompOp	5 math math: norm_jacobiTheta₂_term_fderiv_ge, hasFDerivAt_jacobiTheta₂_term, summable_jacobiTheta₂_term_fderiv_iff, hasSum_jacobiTheta₂_term_fderiv, norm_jacobiTheta₂_term_fderiv_le

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousAt_jacobiTheta₂ 📖	mathematical	Real Real.instLT Real.instZero Complex.im	ContinuousAt Complex instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField jacobiTheta₂	—	HasFDerivAt.continuousAt Prod.continuousAdd IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Prod.continuousSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology hasFDerivAt_jacobiTheta₂
continuousAt_jacobiTheta₂' 📖	mathematical	Real Real.instLT Real.instZero Complex.im	ContinuousAt Complex instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField jacobiTheta₂'	—	exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing NoMaxOrder.exists_gt instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial IsOpen.prod Continuous.isOpen_preimage Continuous.comp continuous_abs Real.instIsOrderedAddMonoid instOrderTopologyReal Complex.continuous_im isOpen_Iio instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal isOpen_Ioi instClosedIicTopology ContinuousOn.continuousAt Nat.instAtLeastTwoHAddOfNat mul_assoc pow_one Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal summable_pow_mul_jacobiTheta₂_term_bound continuousOn_tsum Complex.instCompleteSpace Continuous.continuousOn Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_const continuous_id' Continuous.cexp Continuous.fun_add IsTopologicalSemiring.toContinuousAdd Continuous.fst Continuous.snd norm_jacobiTheta₂'_term_le le_of_lt IsOpen.mem_nhds
differentiableAt_jacobiTheta₂_fst 📖	mathematical	Real Real.instLT Real.instZero Complex.im	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField jacobiTheta₂	—	HasFDerivAt.differentiableAt RingHomCompTriple.ids HasFDerivAt.comp hasFDerivAt_jacobiTheta₂ hasFDerivAt_prodMk_left
differentiableAt_jacobiTheta₂_snd 📖	mathematical	Real Real.instLT Real.instZero Complex.im	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField jacobiTheta₂	—	HasFDerivAt.differentiableAt RingHomCompTriple.ids HasFDerivAt.comp hasFDerivAt_jacobiTheta₂ hasFDerivAt_prodMk_right
hasDerivAt_jacobiTheta₂_fst 📖	mathematical	Real Real.instLT Real.instZero Complex.im	HasDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField IsModuleTopology.toContinuousSMul NontriviallyNormedField.toNormedField Complex.instAdd SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsTopologicalSemiring.toIsModuleTopology Complex.instSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing jacobiTheta₂ jacobiTheta₂'	—	SeminormedAddCommGroup.toIsTopologicalAddGroup IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul Continuous.clm_apply continuous_id' continuous_const ContinuousLinearMap.hasSum hasSum_jacobiTheta₂_term_fderiv RingHomIsometric.ids smul_add mul_one MulZeroClass.mul_zero add_zero mul_comm IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology HasFDerivAt.hasDerivAt RingHomCompTriple.ids HasFDerivAt.comp hasFDerivAt_jacobiTheta₂ hasFDerivAt_prodMk_left HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional
hasFDerivAt_jacobiTheta₂ 📖	mathematical	Real Real.instLT Real.instZero Complex.im	HasFDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Prod.instAddCommGroup Complex.addCommGroup Prod.instModule Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instModuleSelf instTopologicalSpaceProd jacobiTheta₂ jacobiTheta₂_fderiv	—	exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing NoMaxOrder.exists_gt instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial IsOpen.prod Continuous.isOpen_preimage Continuous.comp continuous_abs Real.instIsOrderedAddMonoid instOrderTopologyReal Complex.continuous_im isOpen_Iio instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal isOpen_Ioi instClosedIicTopology IsPreconnected.prod Convex.isPreconnected IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add Convex.inter convex_halfSpace_im_gt convex_halfSpace_im_lt hasFDerivAt_jacobiTheta₂_term Nat.instAtLeastTwoHAddOfNat LE.le.trans norm_jacobiTheta₂_term_fderiv_le mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono norm_jacobiTheta₂_term_le le_of_lt mul_nonneg mul_pos Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul mul_assoc Summable.mul_left instIsTopologicalRingReal summable_pow_mul_jacobiTheta₂_term_bound Summable.of_norm_bounded Complex.instCompleteSpace pow_zero one_mul LT.lt.le hasFDerivAt_tsum_of_isPreconnected instIsRCLikeNormedField
hasFDerivAt_jacobiTheta₂_term 📖	mathematical	—	HasFDerivAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Prod.instAddCommGroup Complex.addCommGroup Prod.instModule Complex.instSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instModuleSelf instTopologicalSpaceProd jacobiTheta₂_term jacobiTheta₂_term_fderiv	—	Nat.instAtLeastTwoHAddOfNat IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul HasFDerivAt.add HasFDerivAt.const_mul hasFDerivAt_fst hasFDerivAt_snd HasFDerivAt.cexp
hasSum_jacobiTheta₂'_term 📖	mathematical	Real Real.instLT Real.instZero Complex.im	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup jacobiTheta₂'_term jacobiTheta₂' SummationFilter.unconditional	—	Summable.hasSum summable_jacobiTheta₂'_term_iff
hasSum_jacobiTheta₂_term 📖	mathematical	Real Real.instLT Real.instZero Complex.im	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup jacobiTheta₂_term jacobiTheta₂ SummationFilter.unconditional	—	Summable.hasSum summable_jacobiTheta₂_term_iff
hasSum_jacobiTheta₂_term_fderiv 📖	mathematical	Real Real.instLT Real.instZero Complex.im	HasSum ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Complex.instModuleSelf ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.topologicalSpace Prod.instAddCommGroup Complex.addCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing jacobiTheta₂_term_fderiv jacobiTheta₂_fderiv SummationFilter.unconditional	—	Summable.hasSum IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup summable_jacobiTheta₂_term_fderiv_iff
jacobiTheta₂'_add_left 📖	mathematical	—	jacobiTheta₂' Complex Complex.instAdd Complex.instOne	—	tsum_congr mul_comm mul_add Distrib.leftDistribClass mul_one Complex.exp_add Complex.exp_int_mul_two_pi_mul_I
jacobiTheta₂'_add_left' 📖	mathematical	—	jacobiTheta₂' Complex Complex.instAdd Complex.instMul Complex.exp Complex.instNeg Complex.ofReal Real.pi Complex.I instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instSub jacobiTheta₂	—	Nat.instAtLeastTwoHAddOfNat le_or_gt jacobiTheta₂_undef jacobiTheta₂'_undef MulZeroClass.mul_zero sub_zero sub_mul mul_comm mul_assoc Complex.exp_add Int.cast_add Int.cast_one mul_add Distrib.leftDistribClass mul_one add_sub_cancel_right Mathlib.Tactic.Ring.of_eq 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_congr 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.add_pf_add_gt Nat.cast_one 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.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.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.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 jacobiTheta₂'.eq_1 tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instT2Space Equiv.tsum_eq sub_add_cancel Summable.tsum_sub SeminormedAddCommGroup.toIsTopologicalAddGroup SummationFilter.instNeBotUnconditional HasSum.summable hasSum_jacobiTheta₂'_term Summable.mul_left hasSum_jacobiTheta₂_term
jacobiTheta₂'_add_right 📖	mathematical	—	jacobiTheta₂' Complex Complex.instAdd instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	tsum_congr Nat.instAtLeastTwoHAddOfNat Complex.exp_add Int.cast_pow 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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Complex.exp_int_mul Complex.exp_two_pi_mul_I one_zpow mul_add Distrib.leftDistribClass mul_one
jacobiTheta₂'_conj 📖	mathematical	—	DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing jacobiTheta₂' Complex.instNeg	—	jacobiTheta₂'_neg_left jacobiTheta₂'.eq_1 Complex.conj_tsum tsum_neg SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Complex.conj_ofReal Complex.conj_I Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.neg_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.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.atom_pf' Mathlib.Tactic.Ring.add_congr 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Tactic.RingNF.add_neg Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat
jacobiTheta₂'_functional_equation 📖	mathematical	—	jacobiTheta₂' Complex Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow Complex.instNeg Complex.I instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.exp Complex.ofReal Real.pi Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instSub jacobiTheta₂	—	Nat.instAtLeastTwoHAddOfNat le_or_gt jacobiTheta₂'_undef neg_div Complex.neg_im one_div Complex.inv_im neg_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing neg_nonneg Complex.normSq_nonneg jacobiTheta₂_undef MulZeroClass.mul_zero sub_zero div_eq_mul_inv neg_one_mul neg_neg div_pos Complex.normSq_pos lt_irrefl Complex.zero_im IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasDerivAt_jacobiTheta₂_fst HasDerivAt.congr_simp IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul mul_comm HasDerivAt.comp hasDerivAt_mul_const HasDerivAt.deriv jacobiTheta₂_functional_equation mul_assoc deriv_const_mul_field deriv_fun_mul DifferentiableAt.cexp DifferentiableAt.mul_const DifferentiableAt.const_mul differentiableAt_pow HasDerivAt.differentiableAt deriv_cexp deriv_mul_const_field deriv_pow_field Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf' 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.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left 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.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_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero 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 Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero Mathlib.Meta.NormNum.isNat_natCast Mathlib.Meta.NormNum.isNat_natSub Mathlib.Tactic.Ring.pow_one_cast Nat.cast_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.sub_congr Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt
jacobiTheta₂'_neg_left 📖	mathematical	—	jacobiTheta₂' Complex Complex.instNeg	—	jacobiTheta₂'.eq_1 tsum_neg SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space Equiv.tsum_eq Equiv.neg_apply neg_mul Int.cast_neg Nat.instAtLeastTwoHAddOfNat 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.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.atom_pf' Mathlib.Tactic.Ring.add_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.intPow_negOfNat_bit0 Mathlib.Meta.NormNum.one_natPow Mathlib.Tactic.Ring.pow_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 mul_one add_zero Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.Ring.one_pow
jacobiTheta₂'_undef 📖	mathematical	Real Real.instLE Complex.im Real.instZero	jacobiTheta₂' Complex Complex.instZero	—	tsum_eq_zero_of_not_summable summable_jacobiTheta₂'_term_iff not_lt
jacobiTheta₂_add_left 📖	mathematical	—	jacobiTheta₂ Complex Complex.instAdd Complex.instOne	—	tsum_congr mul_add Distrib.leftDistribClass Complex.exp_add mul_one mul_comm Complex.exp_int_mul_two_pi_mul_I
jacobiTheta₂_add_left' 📖	mathematical	—	jacobiTheta₂ Complex Complex.instAdd Complex.instMul Complex.exp Complex.instNeg Complex.ofReal Real.pi Complex.I instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat jacobiTheta₂.eq_1 tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instT2Space Equiv.tsum_eq tsum_congr Int.cast_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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_congr 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.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev mul_one add_zero Mathlib.Tactic.RingNF.add_assoc_rev 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.add_pf_add_gt Mathlib.Meta.NormNum.isNat_intCast 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.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf 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
jacobiTheta₂_add_right 📖	mathematical	—	jacobiTheta₂ Complex Complex.instAdd instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	tsum_congr Nat.instAtLeastTwoHAddOfNat Complex.exp_add Int.cast_pow 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.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Complex.exp_int_mul Complex.exp_two_pi_mul_I one_zpow mul_add Distrib.leftDistribClass mul_one
jacobiTheta₂_conj 📖	mathematical	—	DFunLike.coe RingHom Complex Semiring.toNonAssocSemiring CommSemiring.toSemiring Complex.instCommSemiring RingHom.instFunLike starRingEnd Complex.instStarRing jacobiTheta₂ Complex.instNeg	—	jacobiTheta₂_neg_left jacobiTheta₂.eq_1 Complex.conj_tsum mul_neg map_add SemilinearMapClass.toAddHomClass Complex.instCharZero RingHomClass.toLinearMapClassNNRat RingHom.instRingHomClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_ofNat Complex.conj_ofReal Complex.conj_I map_intCast neg_mul neg_neg map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
jacobiTheta₂_fderiv_undef 📖	mathematical	Real Real.instLE Complex.im Real.instZero	jacobiTheta₂_fderiv ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Complex.instModuleSelf ContinuousLinearMap.zero	—	tsum_eq_zero_of_not_summable IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup summable_jacobiTheta₂_term_fderiv_iff not_lt
jacobiTheta₂_functional_equation 📖	mathematical	—	jacobiTheta₂ Complex Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow Complex.instNeg Complex.I instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.exp Complex.ofReal Real.pi Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring	—	Nat.instAtLeastTwoHAddOfNat le_or_gt neg_div Complex.neg_im one_div Complex.inv_im neg_nonpos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing neg_nonneg Complex.normSq_nonneg jacobiTheta₂_undef MulZeroClass.mul_zero neg_mul MulZeroClass.zero_mul one_mul zero_sub neg_neg tsum_congr 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.one_mul Mathlib.Tactic.Ring.pow_congr 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.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 mul_one add_zero 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Complex.tsum_exp_neg_quadratic mul_assoc tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instT2Space Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_div_neg_eq Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.pow_eq_eval Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.zpow'_ofNat Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' mul_neg Mathlib.Tactic.FieldSimp.NF.one_eq_eval Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.div_congr 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.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_neg Complex.I_sq Complex.I_pow_four Nat.cast_one Mathlib.Tactic.Ring.inv_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.of_eq
jacobiTheta₂_neg_left 📖	mathematical	—	jacobiTheta₂ Complex Complex.instNeg	—	jacobiTheta₂.eq_1 Equiv.tsum_eq tsum_congr Int.cast_neg neg_sq mul_assoc neg_mul_neg
jacobiTheta₂_undef 📖	mathematical	Real Real.instLE Complex.im Real.instZero	jacobiTheta₂ Complex Complex.instZero	—	tsum_eq_zero_of_not_summable summable_jacobiTheta₂_term_iff not_lt
norm_jacobiTheta₂'_term_le 📖	mathematical	Real Real.instLT Real.instZero Real.instLE abs Real.lattice Real.instAddGroup Complex.im	Norm.norm Complex Complex.instNorm jacobiTheta₂'_term Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Real.instIntCast instLatticeInt Int.instAddGroup Real.exp Real.instNeg Real.instSub Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat jacobiTheta₂'_term.eq_1 norm_mul NormedDivisionRing.toNormMulClass mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_of_eq Complex.norm_two Complex.norm_of_nonneg LT.lt.le Real.pi_pos Complex.norm_I mul_one Complex.norm_intCast Int.cast_abs Real.instIsStrictOrderedRing norm_jacobiTheta₂_term_le norm_nonneg mul_nonneg le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Int.cast_nonneg IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass abs_nonneg Int.instAddLeftMono covariant_swap_add_of_covariant_add
norm_jacobiTheta₂_term 📖	mathematical	—	Norm.norm Complex Complex.instNorm jacobiTheta₂_term Real.exp Real Real.instSub Real.instMul Real.instNeg Real.pi Monoid.toNatPow Real.instMonoid Real.instIntCast Complex.im instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat jacobiTheta₂_term.eq_1 Complex.norm_exp Complex.ofReal_mul Complex.ofReal_pow Mathlib.Tactic.Ring.of_eq 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.one_mul Mathlib.Tactic.Ring.pow_congr 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.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Complex.add_re Complex.mul_I_re Complex.im_ofReal_mul 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.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.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt
norm_jacobiTheta₂_term_fderiv_ge 📖	mathematical	—	Real Real.instLE Real.instMul Real.pi Monoid.toNatPow Real.instMonoid Real.instIntCast abs instLatticeInt Int.instAddGroup Norm.norm Complex Complex.instNorm jacobiTheta₂_term ContinuousLinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Complex.instModuleSelf ContinuousLinearMap.hasOpNorm Prod.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Prod.normedSpace NontriviallyNormedField.toNormedField InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace jacobiTheta₂_term_fderiv	—	LE.le.trans ContinuousLinearMap.le_opNorm RingHomIsometric.ids NormOneClass.norm_one NormedDivisionRing.to_normOneClass norm_zero max_eq_right zero_le_one Real.instZeroLEOneClass mul_one le_trans smul_zero zero_add mul_comm norm_mul NormedDivisionRing.toNormMulClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_eq Complex.norm_real Real.norm_of_nonneg LT.lt.le Real.pi_pos Complex.norm_I Int.cast_abs Real.instIsStrictOrderedRing norm_pow norm_nonneg
norm_jacobiTheta₂_term_fderiv_le 📖	mathematical	—	Real Real.instLE Norm.norm ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Complex.instModuleSelf ContinuousLinearMap.hasOpNorm Prod.seminormedAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Prod.normedSpace NontriviallyNormedField.toNormedField InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace jacobiTheta₂_term_fderiv Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi Monoid.toNatPow Real.instMonoid Real.instIntCast abs instLatticeInt Int.instAddGroup Complex.instNorm jacobiTheta₂_term	—	Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing norm_smul NormedSpace.toNormSMulClass RingHomIsometric.ids Nat.instAtLeastTwoHAddOfNat jacobiTheta₂_term_fderiv.eq_1 jacobiTheta₂_term.eq_1 mul_comm Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNat_add Nat.cast_one add_mul Distrib.rightDistribClass mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing LE.le.trans norm_add_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add norm_mul NormedDivisionRing.toNormMulClass Complex.norm_real Real.norm_of_nonneg zero_le_two Real.instZeroLEOneClass LT.lt.le Real.pi_pos Complex.norm_I mul_one Real.instIsStrictOrderedRing le_imp_le_of_le_of_le ContinuousLinearMap.norm_fst_le mul_nonneg le_of_lt mul_pos IsStrictOrderedRing.toPosMulStrictMono Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Int.cast_nonneg IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass abs_nonneg Int.instAddLeftMono le_refl Int.cast_mono Int.le_self_sq one_mul Int.cast_abs abs_pow mul_le_of_le_one_right pow_nonneg ContinuousLinearMap.norm_snd_le norm_nonneg
norm_jacobiTheta₂_term_le 📖	mathematical	Real Real.instLT Real.instZero Real.instLE abs Real.lattice Real.instAddGroup Complex.im	Norm.norm Complex Complex.instNorm jacobiTheta₂_term Real.exp Real.instMul Real.instNeg Real.pi Real.instSub Monoid.toNatPow Real.instMonoid Real.instIntCast instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat instLatticeInt Int.instAddGroup	—	Nat.instAtLeastTwoHAddOfNat norm_jacobiTheta₂_term sub_eq_add_neg neg_mul IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add mul_comm mul_assoc Distrib.leftDistribClass mul_le_mul_iff_right₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.pi_pos add_le_add mul_le_mul IsOrderedRing.toMulPosMono le_rfl LT.lt.le sq_nonneg AddGroup.existsAddOfLE mul_neg two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike le_trans neg_le_neg_iff abs_mul Int.cast_abs mul_le_mul_of_nonneg_left abs_nonneg neg_abs_le
summable_jacobiTheta₂'_term_iff 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup jacobiTheta₂'_term SummationFilter.unconditional Real Real.instLT Real.instZero Complex.im	—	summable_jacobiTheta₂_term_iff Summable.of_norm_bounded_eventually Complex.instCompleteSpace Nat.instAtLeastTwoHAddOfNat Summable.mul_left IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Summable.norm Complex.instFiniteDimensionalReal Filter.mem_sup Filter.eventually_ne_atBot instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Int.cofinite_eq Filter.mp_mem Filter.univ_mem' jacobiTheta₂'_term.eq_1 norm_mul NormedDivisionRing.toNormMulClass mul_assoc le_mul_of_one_le_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg Complex.norm_I Complex.norm_real mul_one Real.norm_of_nonneg LT.lt.le Real.pi_pos two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instIsStrictOrderedRing inv_mul_cancel₀ LT.lt.ne' mul_pos IsStrictOrderedRing.toPosMulStrictMono one_mul Int.cast_one Int.cast_le Int.one_le_abs Summable.of_norm_bounded summable_pow_mul_jacobiTheta₂_term_bound pow_one mul_le_mul IsOrderedRing.toPosMulMono le_of_eq Complex.norm_two Complex.norm_of_nonneg Complex.norm_intCast Int.cast_abs norm_jacobiTheta₂_term_le le_rfl mul_nonneg le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Int.cast_nonneg IsOrderedRing.toIsOrderedAddMonoid IsOrderedRing.toZeroLEOneClass abs_nonneg Int.instAddLeftMono covariant_swap_add_of_covariant_add
summable_jacobiTheta₂_term_fderiv_iff 📖	mathematical	—	Summable ContinuousLinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring instTopologicalSpaceProd UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Prod.instAddCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Prod.instModule Complex.instModuleSelf ContinuousLinearMap.addCommMonoid IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap.topologicalSpace Prod.instAddCommGroup Complex.addCommGroup SeminormedAddCommGroup.toIsTopologicalAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing jacobiTheta₂_term_fderiv SummationFilter.unconditional Real Real.instLT Real.instZero Complex.im	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing SeminormedAddCommGroup.toIsTopologicalAddGroup summable_jacobiTheta₂_term_iff RingHomIsometric.ids Summable.norm IsScalarTower.to_smulCommClass' IsScalarTower.right Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.complexToReal Algebra.to_smulCommClass UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul ContinuousLinearMap.instModuleFinite Prod.instModuleIsReflexive FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self IsSimpleModule.instIsNoetherian instIsSimpleModule Module.Free.of_divisionRing Summable.of_norm_bounded_eventually Complex.instCompleteSpace Filter.mem_sup Filter.eventually_ne_atBot instNoBotOrderOfNoMinOrder instNoMinOrderOfNontrivial IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.instNontrivial Filter.eventually_ne_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Int.cofinite_eq Filter.mp_mem Filter.univ_mem' le_trans le_mul_of_one_le_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg LE.le.trans Nat.instAtLeastTwoHAddOfNat Real.one_le_pi_div_two mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Mathlib.Meta.NormNum.isRat_le_true Real.instIsStrictOrderedRing Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one one_le_sq_iff_one_le_abs Int.cast_abs abs_abs Int.instAddLeftMono covariant_swap_add_of_covariant_add Int.cast_one Int.cast_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one Int.one_le_abs LT.lt.le Real.pi_pos norm_jacobiTheta₂_term_fderiv_ge Summable.of_norm_bounded ContinuousLinearMap.instCompleteSpace Prod.instIsTopologicalAddGroup Prod.continuousSMul IsModuleTopology.toContinuousSMul IsTopologicalSemiring.toIsModuleTopology FrechetUrysohnSpace.to_sequentialSpace FirstCountableTopology.frechetUrysohnSpace TopologicalSpace.instFirstCountableTopologyProd TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology PseudoEMetricSpace.pseudoMetrizableSpace Summable.mul_left instIsTopologicalRingReal summable_pow_mul_jacobiTheta₂_term_bound norm_jacobiTheta₂_term_fderiv_le mul_assoc norm_jacobiTheta₂_term_le le_rfl pow_nonneg Int.cast_nonneg abs_nonneg mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.instNontrivial
summable_jacobiTheta₂_term_iff 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup jacobiTheta₂_term SummationFilter.unconditional Real Real.instLT Real.instZero Complex.im	—	Summable.of_norm_bounded Complex.instCompleteSpace Nat.instAtLeastTwoHAddOfNat summable_pow_mul_jacobiTheta₂_term_bound pow_zero one_mul norm_jacobiTheta₂_term_le le_rfl lt_or_eq_of_le norm_jacobiTheta₂_term Int.cast_natCast Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr 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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_gt 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 Filter.Tendsto.comp Real.tendsto_exp_atTop Filter.Tendsto.atTop_mul_atTop₀ Real.instIsOrderedRing tendsto_natCast_atTop_atTop Real.instArchimedean Filter.tendsto_atTop_add_const_right Real.instIsOrderedAddMonoid Filter.Tendsto.atTop_mul_const Real.instIsStrictOrderedRing mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd Real.pi_pos Filter.Tendsto.norm Summable.tendsto_atTop_zero SeminormedAddCommGroup.toIsTopologicalAddGroup Summable.comp_injective SeminormedAddCommGroup.to_isUniformAddGroup Filter.NeBot.ne Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat disjoint_self Filter.Tendsto.disjoint disjoint_nhds_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instNontrivial instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal lt_trichotomy instIsTopologicalAddGroupReal instIsUniformAddGroupReal Real.instCompleteSpace zero_sub MulZeroClass.mul_zero summable_norm_iff Complex.instFiniteDimensionalReal mul_assoc Filter.Tendsto.const_mul_atBot two_pos Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Filter.Tendsto.atTop_mul_const_of_neg neg_zero Real.exp_zero Int.infinite TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace one_ne_zero Int.instCharZero neg_neg neg_mul mul_neg Int.cast_neg Filter.Tendsto.const_mul_atTop mul_pos IsStrictOrderedRing.toPosMulStrictMono
summable_pow_mul_jacobiTheta₂_term_bound 📖	mathematical	Real Real.instLT Real.instZero	Summable Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instMul Monoid.toNatPow Real.instMonoid Real.instIntCast abs instLatticeInt Int.instAddGroup Real.exp Real.instNeg Real.pi Real.instSub instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat summable_of_isBigO_nat Real.instCompleteSpace Real.summable_pow_mul_exp_neg_nat_mul zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Asymptotics.IsBigO.mul NormedDivisionRing.toNormMulClass Asymptotics.isBigO_refl Real.isBigO_exp_comp_exp_comp Filter.Tendsto.isBoundedUnder_le_atBot Real.instIsOrderedAddMonoid Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_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.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Nat.cast_one Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Filter.Tendsto.atTop_mul_atTop₀ Real.instIsOrderedRing tendsto_natCast_atTop_atTop Real.instArchimedean Filter.tendsto_atTop_add_const_right Filter.Tendsto.const_mul_atTop Real.instIsStrictOrderedRing mul_pos IsStrictOrderedRing.toPosMulStrictMono Real.pi_pos Summable.of_nat_of_neg instIsTopologicalAddGroupReal Nat.abs_cast IsStrictOrderedRing.toIsOrderedRing Int.instIsStrictOrderedRing Int.cast_natCast abs_neg Int.cast_neg neg_sq

---

← Back to Index