QExpansion

📁 Source: Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

Statistics

Metric	Count
Definitions	0
Theorems qExpansion_identity, qExpansion_identity_pnat, q_expansion_bernoulli, q_expansion_riemannZeta, contDiffOn_tsum_cexp, differentiableAt_iteratedDerivWithin_cexp, eisSummand_of_gammaSet_eq_divIntMap, iteratedDerivWithin_tsum_cexp_eq, summableLocallyUniformlyOn_iteratedDerivWithin_cexp, summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp, summable_eisSummand, summable_pow_mul_cexp, summable_prod_eisSummand, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow	15
Total	15

EisensteinSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
qExpansion_identity 📖	mathematical	—	tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd UpperHalfPlane.coe Complex.instIntCast SummationFilter.unconditional Complex.instMul Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Nat.factorial Complex.exp	—	Nat.instAtLeastTwoHAddOfNat iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow UpperHalfPlane.coe_im_pos iteratedDerivWithin_congr pi_mul_cot_pi_q_exp eq_inv_mul_iff_mul_eq₀ NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass isReduced_of_noZeroDivisors Complex.instNontrivial NeZero.charZero_one Complex.instCharZero IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instT2Space neg_pow Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul neg_mul mul_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.inv_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_mul Mathlib.Tactic.FieldSimp.eq_div_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div' div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg Mathlib.Meta.NormNum.isInt_eq_false Mathlib.Meta.NormNum.isInt_neg Nat.cast_one Nat.cast_zero Mathlib.Tactic.FieldSimp.NF.cons_ne_zero CharZero.NeZero.two one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg add_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.RingNF.mul_assoc_rev Even.neg_pow one_pow
qExpansion_identity_pnat 📖	mathematical	—	tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instAdd UpperHalfPlane.coe Complex.instIntCast SummationFilter.unconditional Complex.instMul Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Nat.factorial PNat PNat.val Complex.exp	—	Nat.instAtLeastTwoHAddOfNat qExpansion_identity tsum_zero_pnat_eq_tsum_nat SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space Summable.congr summable_pow_mul_cexp Nat.cast_one mul_one neg_mul CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero zero_pow pow_zero zero_add
q_expansion_bernoulli 📖	mathematical	Even	DFunLike.coe ModularForm Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing CongruenceSubgroup.Gamma UpperHalfPlane Complex ModularForm.funLike ModularForm.E Complex.instSub Complex.instOne Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instRatCast bernoulli tsum PNat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass ArithmeticFunction.instFunLikeNat ArithmeticFunction.sigma PNat.val DivInvMonoid.toZPow Complex.exp Complex.ofReal Real.pi Complex.I UpperHalfPlane.coe SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat neg_mul sub_eq_add_neg q_expansion_riemannZeta
q_expansion_riemannZeta 📖	mathematical	Even	DFunLike.coe ModularForm Subgroup.map Matrix.SpecialLinearGroup Fin.fintype Int.instCommRing Matrix.SpecialLinearGroup.instGroup Matrix.GeneralLinearGroup Real Real.semiring Units.instGroup Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Matrix.SpecialLinearGroup.mapGL Real.commRing Ring.toIntAlgebra Real.instRing CongruenceSubgroup.Gamma UpperHalfPlane Complex ModularForm.funLike ModularForm.E Complex.instAdd Complex.instOne Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instInv riemannZeta Complex.instNatCast Monoid.toNatPow Complex.instSemiring Complex.instNeg instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I Nat.factorial tsum PNat ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass ArithmeticFunction.instFunLikeNat ArithmeticFunction.sigma PNat.val DivInvMonoid.toZPow Complex.exp UpperHalfPlane.coe SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat ModularForm.E.eq_1 ModularForm.IsGLPos.smul_apply eisensteinSeriesSIF_apply eisensteinSeries.eq_1 tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries riemannZeta_ne_zero_of_one_lt_re Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike one_div zpow_neg zpow_natCast neg_mul inv_mul_eq_iff_eq_mul₀

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
contDiffOn_tsum_cexp 📖	mathematical	—	ContDiffOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex WithTop.some ENat tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.exp Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I SummationFilter.unconditional UpperHalfPlane.upperHalfPlaneSet	—	contDiffOn_of_differentiableOn_deriv Nat.instAtLeastTwoHAddOfNat DifferentiableWithinAt.congr SummableLocallyUniformlyOn.differentiableOn Complex.instCompleteSpace UpperHalfPlane.isOpen_upperHalfPlaneSet summableLocallyUniformlyOn_iteratedDerivWithin_cexp differentiableAt_iteratedDerivWithin_cexp iteratedDerivWithin_tsum_cexp_eq
differentiableAt_iteratedDerivWithin_cexp 📖	mathematical	IsOpen Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex Set Set.instMembership	DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf iteratedDerivWithin Complex.instNormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra CommCStarAlgebra.toNonUnitalCommCStarAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.exp Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I	—	DifferentiableOn.differentiableAt Nat.instAtLeastTwoHAddOfNat Differentiable.differentiableOn ContDiff.differentiable_iteratedDeriv' ContDiff.pow ContDiff.cexp ContDiff.mul contDiff_const contDiff_fun_id DifferentiableOn.congr iteratedDerivWithin_of_isOpen IsOpen.mem_nhds
eisSummand_of_gammaSet_eq_divIntMap 📖	mathematical	—	EisensteinSeries.eisSummand Set Set.instMembership EisensteinSeries.gammaSet Pi.instZero ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing Complex Complex.instMul Complex.instInv DivInvMonoid.toZPow Complex.instDivInvMonoid Complex.instNatCast EisensteinSeries.divIntMap	—	EisensteinSeries.gammaSet_eq_gcd_mul_divIntMap Int.cast_natCast Int.cast_mul mul_assoc zpow_neg mul_add Distrib.leftDistribClass
iteratedDerivWithin_tsum_cexp_eq 📖	mathematical	—	iteratedDerivWithin Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.exp Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I SummationFilter.unconditional UpperHalfPlane.upperHalfPlaneSet UpperHalfPlane.coe	—	Nat.instAtLeastTwoHAddOfNat iteratedDerivWithin_tsum instIsRCLikeNormedField UpperHalfPlane.isOpen_upperHalfPlaneSet UpperHalfPlane.coe_im_pos summable_geometric_iff_norm_lt_one UpperHalfPlane.norm_exp_two_pi_I_lt_one summableLocallyUniformlyOn_iteratedDerivWithin_cexp differentiableAt_iteratedDerivWithin_cexp
summableLocallyUniformlyOn_iteratedDerivWithin_cexp 📖	mathematical	—	SummableLocallyUniformlyOn Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra CommCStarAlgebra.toNonUnitalCommCStarAlgebra Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.exp Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I UpperHalfPlane.upperHalfPlaneSet	—	NormOneClass.norm_one NormedDivisionRing.to_normOneClass norm_pow NormedDivisionRing.toNormMulClass Real.norm_natCast instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Nat.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike pow_one one_mul Nat.instAtLeastTwoHAddOfNat div_one one_smul summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp Mathlib.Meta.NormNum.isNat_lt_true Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero
summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp 📖	mathematical	Real Real.instLT Real.instZero Asymptotics.IsBigO Complex Complex.instNorm Real.norm Filter.atTop Nat.instPreorder Monoid.toNatPow Real.instMonoid Real.instNatCast	SummableLocallyUniformlyOn ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Function.hasSMul Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id iteratedDerivWithin DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NonUnitalCStarAlgebra.toNormedSpace NonUnitalCommCStarAlgebra.toNonUnitalCStarAlgebra CommCStarAlgebra.toNonUnitalCommCStarAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.exp DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I UpperHalfPlane.upperHalfPlaneSet	—	SummableLocallyUniformlyOn_of_locally_bounded Complex.instCompleteSpace locallyCompact_of_proper Complex.instProperSpace Nat.instAtLeastTwoHAddOfNat UpperHalfPlane.isOpen_upperHalfPlaneSet isCompact_univ_iff isCompact_iff_isCompact_univ Continuous.cexp Continuous.comp' Continuous.div_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing continuous_id' Continuous.fun_mul continuous_const continuous_subtype_val norm_norm BoundedContinuousFunction.norm_lt_iff_of_compact Real.zero_lt_one 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.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Tactic.Ring.inv_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_inv_pos Complex.instCharZero Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero UpperHalfPlane.norm_exp_two_pi_I_lt_one Complex.div_ofReal_im PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Complex.norm_mul norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Complex.norm_div Complex.norm_ofNat Complex.norm_real Complex.norm_I mul_one RCLike.norm_natCast norm_mul norm_div Real.norm_ofNat abs_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add summable_norm_mul_geometric_of_norm_lt_one' Asymptotics.isBigO_norm_left pow_le_pow_left₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono norm_nonneg BoundedContinuousFunction.norm_coe_le_norm Complex.norm_natCast abs_norm mul_assoc mul_le_mul_of_nonneg_left Complex.exp_nsmul' mul_nonneg pow_nonneg IsOrderedRing.toZeroLEOneClass Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos le_of_lt mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial abs_pos_of_pos Real.pi_pos Nat.cast_nonneg' Real.instZeroLEOneClass
summable_eisSummand 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup EisensteinSeries.eisSummand SummationFilter.unconditional	—	summable_norm_iff Complex.instFiniteDimensionalReal EisensteinSeries.summable_norm_eisSummand
summable_pow_mul_cexp 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNatCast Complex.exp instOfNatAtLeastTwo Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I PNat.val UpperHalfPlane.coe SummationFilter.unconditional	—	MulZeroClass.zero_mul add_zero IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.instIsOrderedRing Real.instNontrivial UpperHalfPlane.coe_im_pos Summable.congr Nat.instAtLeastTwoHAddOfNat SummableLocallyUniformlyOn.summable summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Nat.cast_one Complex.ofReal_pow
summable_prod_eisSummand 📖	mathematical	—	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup EisensteinSeries.eisSummand Matrix.vecCons Matrix.vecEmpty SummationFilter.unconditional	—	Equiv.summable_iff Summable.congr summable_eisSummand
tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries 📖	mathematical	—	tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup EisensteinSeries.eisSummand SummationFilter.unconditional Complex.instMul riemannZeta Complex.instNatCast eisensteinSeries Pi.instZero ZMod MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ZMod.commRing	—	Int.instAddLeftMono Int.instZeroLEOneClass Int.instCharZero Equiv.tsum_eq eisensteinSeries.eq_1 Summable.tsum_sigma SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Summable.congr Equiv.summable_iff Summable.of_norm EisensteinSeries.summable_norm_eisSummand zeta_nat_eq_tsum_of_gt_one tsum_mul_tsum_of_summable_norm one_div norm_inv norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass RCLike.norm_natCast Summable.subtype instIsUniformAddGroupReal Real.instCompleteSpace Summable.tsum_prod' IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing T4Space.t3Space T4Space.of_paracompactSpace_t2Space Complex.instT2Space Metric.instParacompactSpace summable_mul_of_summable_norm Summable.mul_left tsum_congr eq_or_ne eisSummand_of_gammaSet_eq_divIntMap CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero zpow_natCast isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Complex.instNontrivial Nat.instCanonicallyOrderedAdd Nat.instCharZero Nat.instAtLeastTwoHAddOfNat MulZeroClass.zero_mul tsum_zero Nat.cast_one one_pow inv_one one_mul tsum_mul_left IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain
tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow 📖	mathematical	Even	tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing CommCStarAlgebra.toNormedCommRing instCommCStarAlgebraComplex ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup EisensteinSeries.eisSummand SummationFilter.unconditional Complex.instAdd Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat riemannZeta DivInvMonoid.toDiv Complex.instDivInvMonoid Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instNeg Complex.ofReal Real.pi Complex.I Nat.factorial PNat DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass ArithmeticFunction.instFunLikeNat ArithmeticFunction.sigma PNat.val Complex.exp UpperHalfPlane.coe	—	Nat.instAtLeastTwoHAddOfNat Equiv.tsum_eq finTwoArrowEquiv_symm_apply Summable.tsum_prod SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace T6Space.toT0Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace summable_prod_eisSummand tsum_int_eq_zero_add_two_mul_tsum_pnat Complex.instT2Space tsum_comp_neg tsum_congr Int.cast_neg neg_mul Matrix.cons_val_fin_one neg_add zpow_neg zpow_natCast Even.neg_pow Summable.prod MulZeroClass.zero_mul add_zero IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Real.instIsOrderedRing Real.instNontrivial UpperHalfPlane.coe_im_pos EisensteinSeries.qExpansion_identity_pnat nsmul_eq_mul mul_assoc Int.cast_zero zero_add two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even tsum_congr₂ Nat.cast_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right 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.atom_pf' Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.mul_assoc_rev mul_one Int.cast_natCast one_div tsum_mul_left IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing tsum_prod_pow_eq_tsum_sigma RCLike.instNormSMulClassInt UpperHalfPlane.norm_exp_two_pi_I_lt_one

---

← Back to Index