QExpansion

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

Statistics

Metric	Count
Definitions qExpansion, qExpansionFormalMultilinearSeries, cuspFunction, valueAtInfty, qExpansionAddHom, qExpansionRingHom	6
Theorems cuspFunction_apply_zero, exp_decay_atImInfty, exp_decay_atImInfty', zero_at_infty_comp_ofComplex, cuspFunction_mul, qExpansion_mul, analyticAt_cuspFunction_zero, bounded_at_infty_comp_ofComplex, cuspFunction_apply_zero, differentiableAt_comp_ofComplex, differentiableAt_cuspFunction, differentiableOn_cuspFunction_ball, exp_decay_sub_atImInfty, exp_decay_sub_atImInfty', hasFPowerSeries_cuspFunction, hasSum_qExpansion, hasSum_qExpansion_of_abs_lt, hasSum_qExpansion_of_norm_lt, qExpansionFormalMultilinearSeries_apply_norm, qExpansionFormalMultilinearSeries_coeff, qExpansionFormalMultilinearSeries_radius, qExpansion_coeff, qExpansion_coeff_eq_circleIntegral, qExpansion_coeff_eq_intervalIntegral, qExpansion_coeff_zero, eq_cuspFunction, periodic_comp_ofComplex, cuspFunction_apply_zero, exp_decay_atImInfty, exp_decay_atImInfty', valueAtInfty_eq_zero, zero_at_infty_comp_ofComplex, qParam_tendsto_atImInfty, cuspFunction_add, cuspFunction_mul, cuspFunction_mul_zero, cuspFunction_neg, cuspFunction_smul, cuspFunction_sub, hasFPowerSeriesOnBall_cuspFunction, qExpansionRingHom_apply, qExpansion_add, qExpansion_coeff_unique, qExpansion_eq_zero_iff, qExpansion_mul, qExpansion_mul_coeff_zero, qExpansion_neg, qExpansion_of_mul, qExpansion_of_pow, qExpansion_one, qExpansion_smul, qExpansion_sub, qExpansion_zero	53
Total	59

CuspFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cuspFunction_apply_zero 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	SlashInvariantFormClass.cuspFunction DFunLike.coe UpperHalfPlane Complex Complex.instZero	—	Subgroup.isCusp_of_mem_strictPeriods UpperHalfPlane.IsZeroAtImInfty.cuspFunction_apply_zero zero_at_infty
exp_decay_atImInfty 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	Asymptotics.IsBigO UpperHalfPlane Complex Complex.instNorm Real.norm UpperHalfPlane.atImInfty DFunLike.coe Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi UpperHalfPlane.im	—	Subgroup.isCusp_of_mem_strictPeriods UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty CuspForm.instModularFormClassOfCuspFormClass zero_at_infty
exp_decay_atImInfty' 📖	mathematical	—	Real Real.instLT Real.instZero Asymptotics.IsBigO UpperHalfPlane Complex Complex.instNorm Real.norm UpperHalfPlane.atImInfty DFunLike.coe Real.exp Real.instMul Real.instNeg UpperHalfPlane.im	—	UpperHalfPlane.IsZeroAtImInfty.exp_decay_atImInfty' CuspForm.instModularFormClassOfCuspFormClass zero_at_infty
zero_at_infty_comp_ofComplex 📖	mathematical	—	Filter.ZeroAtFilter Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Filter.comap Real Complex.im Filter.atTop Real.instPreorder UpperHalfPlane DFunLike.coe OpenPartialHomeomorph.toFun' UpperHalfPlane.instTopologicalSpace UpperHalfPlane.ofComplex	—	Filter.Tendsto.comp zero_at_infty UpperHalfPlane.tendsto_comap_im_ofComplex

ModularForm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cuspFunction_mul 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	SlashInvariantFormClass.cuspFunction DFunLike.coe ModularForm UpperHalfPlane Complex funLike mul Pi.instMul Complex.instMul	—	cuspFunction_mul AnalyticAt.continuousAt ModularFormClass.analyticAt_cuspFunction_zero ModularFormClass.modularForm
qExpansion_mul 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion DFunLike.coe ModularForm UpperHalfPlane Complex funLike mul PowerSeries MvPowerSeries.instMul Complex.instSemiring	—	qExpansion_mul ModularFormClass.analyticAt_cuspFunction_zero ModularFormClass.modularForm

ModularFormClass

Definitions

Name	Category	Theorems
qExpansion 📖	CompOp	26 math math: CuspFormClass.qExpansion_isBigO, qExpansionFormalMultilinearSeries_apply_norm, qExpansion_eq_zero_iff, qExpansionRingHom_apply, qExpansion_of_mul, qExpansion_one, qExpansion_coeff, qExpansion_sub, qExpansion_coeff_zero, qExpansion_add, hasSum_qExpansion_of_abs_lt, qExpansion_coeff_eq_circleIntegral, qExpansion_neg, qExpansion_isBigO, qExpansion_mul, qExpansion_mul_coeff_zero, hasSum_qExpansion_of_norm_lt, qExpansion_coeff_unique, ModularForm.qExpansion_mul, qExpansion_zero, qExpansionFormalMultilinearSeries_coeff, qExpansion_of_pow, qExpansion_smul, hasSum_qExpansion, qExpansion_coeff_isBigO_of_norm_isBigO, qExpansion_coeff_eq_intervalIntegral
qExpansionFormalMultilinearSeries 📖	CompOp	4 math math: qExpansionFormalMultilinearSeries_apply_norm, hasFPowerSeries_cuspFunction, qExpansionFormalMultilinearSeries_radius, qExpansionFormalMultilinearSeries_coeff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
analyticAt_cuspFunction_zero 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SlashInvariantFormClass.cuspFunction DFunLike.coe UpperHalfPlane Complex.instZero	—	DifferentiableOn.analyticAt Complex.instCompleteSpace DifferentiableAt.differentiableWithinAt differentiableAt_cuspFunction ball_zero_eq Metric.ball_mem_nhds zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
bounded_at_infty_comp_ofComplex 📖	mathematical	IsCusp OnePoint.infty Real	Filter.BoundedAtFilter Complex Complex.instNorm Filter.comap Complex.im Filter.atTop Real.instPreorder UpperHalfPlane DFunLike.coe OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField UpperHalfPlane.instTopologicalSpace UpperHalfPlane.ofComplex	—	Asymptotics.IsBigO.comp_tendsto OnePoint.isBoundedAt_infty_iff bdd_at_cusps UpperHalfPlane.tendsto_comap_im_ofComplex
cuspFunction_apply_zero 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	SlashInvariantFormClass.cuspFunction DFunLike.coe UpperHalfPlane Complex Complex.instZero UpperHalfPlane.valueAtInfty	—	Filter.Tendsto.limUnder_eq Complex.instT2Space UpperHalfPlane.instNeBotAtImInfty SlashInvariantFormClass.eq_cuspFunction toSlashInvariantFormClass LT.lt.ne' Filter.Tendsto.comp ContinuousAt.tendsto AnalyticAt.continuousAt analyticAt_cuspFunction_zero UpperHalfPlane.qParam_tendsto_atImInfty
differentiableAt_comp_ofComplex 📖	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 UpperHalfPlane DFunLike.coe OpenPartialHomeomorph.toFun' UpperHalfPlane.instTopologicalSpace UpperHalfPlane.ofComplex	—	mdifferentiableAt_iff_differentiableAt MDifferentiableAt.comp holo UpperHalfPlane.mdifferentiableAt_ofComplex
differentiableAt_cuspFunction 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods Norm.norm Complex Complex.instNorm Real.instOne	DifferentiableAt DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction DFunLike.coe UpperHalfPlane	—	eq_or_ne Function.Periodic.differentiableAt_cuspFunction_zero SlashInvariantFormClass.periodic_comp_ofComplex toSlashInvariantFormClass Filter.eventually_of_mem Filter.preimage_mem_comap Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial differentiableAt_comp_ofComplex bounded_at_infty_comp_ofComplex Subgroup.isCusp_of_mem_strictPeriods Function.Periodic.differentiableAt_cuspFunction LT.lt.ne' Function.Periodic.qParam_right_inv Function.Periodic.im_invQParam_pos_of_norm_lt_one
differentiableOn_cuspFunction_ball 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	DifferentiableOn Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction DFunLike.coe UpperHalfPlane Metric.ball Complex.instZero Real.instOne	—	DifferentiableAt.differentiableWithinAt differentiableAt_cuspFunction mem_ball_zero_iff
exp_decay_sub_atImInfty 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	Asymptotics.IsBigO UpperHalfPlane Complex Complex.instNorm Real.norm UpperHalfPlane.atImInfty Complex.instSub DFunLike.coe UpperHalfPlane.valueAtInfty Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi UpperHalfPlane.im	—	Subgroup.isCusp_of_mem_strictPeriods Nat.instAtLeastTwoHAddOfNat cuspFunction_apply_zero UpperHalfPlane.ofComplex_apply Asymptotics.IsBigO.comp_tendsto Function.Periodic.exp_decay_sub_of_bounded_at_inf SlashInvariantFormClass.periodic_comp_ofComplex toSlashInvariantFormClass Filter.eventually_of_mem Filter.preimage_mem_comap Filter.Ioi_mem_atTop instNoTopOrderOfNoMaxOrder instNoMaxOrderOfNontrivial Real.instIsOrderedRing Real.instNontrivial differentiableAt_comp_ofComplex bounded_at_infty_comp_ofComplex UpperHalfPlane.tendsto_coe_atImInfty
exp_decay_sub_atImInfty' 📖	mathematical	—	Real Real.instLT Real.instZero Asymptotics.IsBigO UpperHalfPlane Complex Complex.instNorm Real.norm UpperHalfPlane.atImInfty Complex.instSub DFunLike.coe UpperHalfPlane.valueAtInfty Real.exp Real.instMul Real.instNeg UpperHalfPlane.im	—	Subgroup.strictWidthInfty_pos_iff Subgroup.instDiscreteTopStrictPeriods instIsTopologicalRingReal Fact.out Subgroup.strictWidthInfty_mem_strictPeriods Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Real.two_pi_pos Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.div_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.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 RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_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.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 add_zero exp_decay_sub_atImInfty
hasFPowerSeries_cuspFunction 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	HasFPowerSeriesOnBall Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SlashInvariantFormClass.cuspFunction DFunLike.coe UpperHalfPlane qExpansionFormalMultilinearSeries Complex.instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	qExpansionFormalMultilinearSeries_radius zero_lt_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.charZero_one ENNReal.instCharZero FormalMultilinearSeries.apply_eq_prod_smul_coeff Finset.prod_const Fintype.card_fin FormalMultilinearSeries.coeff_ofScalars zero_add mul_comm hasSum_qExpansion_of_norm_lt coe_nnnorm NNReal.coe_lt_one ENNReal.coe_lt_one_iff enorm_eq_nnnorm edist_zero_right Metric.mem_eball
hasSum_qExpansion 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id DFunLike.coe LinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Function.Periodic.qParam UpperHalfPlane.coe SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos UpperHalfPlane.im_pos Complex.norm_exp Complex.div_ofReal_re MulZeroClass.mul_zero sub_zero MulZeroClass.zero_mul add_zero mul_one sub_self zero_sub neg_div IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid SlashInvariantFormClass.eq_cuspFunction toSlashInvariantFormClass LT.lt.ne' hasSum_qExpansion_of_norm_lt
hasSum_qExpansion_of_abs_lt 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods Norm.norm Complex Complex.instNorm Real.instOne	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id DFunLike.coe LinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SlashInvariantFormClass.cuspFunction SummationFilter.unconditional	—	hasSum_qExpansion_of_norm_lt
hasSum_qExpansion_of_norm_lt 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods Norm.norm Complex Complex.instNorm Real.instOne	HasSum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id DFunLike.coe LinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero SlashInvariantFormClass.cuspFunction SummationFilter.unconditional	—	Complex.hasSum_taylorSeries_on_ball Complex.instCompleteSpace differentiableOn_cuspFunction_ball dist_zero_right
qExpansionFormalMultilinearSeries_apply_norm 📖	mathematical	—	Norm.norm ContinuousMultilinearMap Complex 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 ContinuousMultilinearMap.hasOpNorm' DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace Complex.instRCLike RCLike.innerProductSpace Fin.fintype qExpansionFormalMultilinearSeries Complex.instNorm DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane	—	IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul qExpansionFormalMultilinearSeries.eq_1 RingHomInvPair.ids SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul smulCommClass_self LinearIsometryEquiv.norm_map FormalMultilinearSeries.norm_apply_eq_norm_coef FormalMultilinearSeries.coeff_ofScalars
qExpansionFormalMultilinearSeries_coeff 📖	mathematical	—	FormalMultilinearSeries.coeff Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace qExpansionFormalMultilinearSeries DFunLike.coe LinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane	—	FormalMultilinearSeries.coeff_ofScalars
qExpansionFormalMultilinearSeries_radius 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal FormalMultilinearSeries.radius Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace qExpansionFormalMultilinearSeries	—	le_of_forall_lt_imp_le_of_dense ENNReal.instDenselyOrdered CanLift.prf ENNReal.canLift LT.lt.ne_top FormalMultilinearSeries.le_radius_of_summable qExpansionFormalMultilinearSeries_apply_norm NNReal.abs_eq NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass Summable.norm FiniteDimensional.rclike_to_real HasSum.summable hasSum_qExpansion_of_norm_lt Complex.norm_real
qExpansion_coeff 📖	mathematical	—	DFunLike.coe LinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion Complex.instMul Complex.instInv Complex.instNatCast Nat.factorial iteratedDeriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SlashInvariantFormClass.cuspFunction Complex.instZero	—	—
qExpansion_coeff_eq_circleIntegral 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods Real.instOne	DFunLike.coe LinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane Complex.instMul Complex.instInv instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.ofReal Real.pi Complex.I circleIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace DivInvMonoid.toDiv Complex.instDivInvMonoid SlashInvariantFormClass.cuspFunction Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instZero	—	Nat.instAtLeastTwoHAddOfNat DifferentiableOn.circleIntegral_one_div_sub_center_pow_smul Complex.instCompleteSpace DifferentiableOn.mono differentiableOn_cuspFunction_ball Metric.closedBall_subset_ball div_eq_iff Complex.two_pi_I_ne_zero mul_comm mul_assoc div_eq_mul_inv smul_eq_mul sub_zero one_div_mul_eq_div div_eq_inv_mul
qExpansion_coeff_eq_intervalIntegral 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	DFunLike.coe LinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane Complex.instMul DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.ofReal intervalIntegral Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup instInnerProductSpaceRealComplex Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Function.Periodic.qParam Complex.instAdd Complex.I MeasureTheory.MeasureSpace.volume Real.measureSpace	—	Nat.instAtLeastTwoHAddOfNat Real.exp_pos Real.exp_lt_one_iff neg_mul neg_div IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing mul_pos Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Real.pi_pos qExpansion_coeff_eq_circleIntegral circleIntegral.eq_1 Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_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 one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero ne_of_gt Mathlib.Tactic.FieldSimp.NF.cons_ne_zero Mathlib.Meta.NormNum.isNat_eq_false RCLike.charZero_rclike Nat.cast_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial MulZeroClass.zero_mul MulZeroClass.mul_zero add_zero zero_add Complex.ofReal_exp Complex.ofReal_div Complex.ofReal_mul Complex.ofReal_neg Complex.I_sq deriv_circleMap UpperHalfPlane.coe_im_pos SlashInvariantFormClass.eq_cuspFunction toSlashInvariantFormClass LT.lt.ne' pow_succ Mathlib.Tactic.FieldSimp.NF.inv_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_mul_eval_cons Complex.instCharZero Complex.exp_ne_zero 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' Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.one_eq_eval isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
qExpansion_coeff_zero 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	DFunLike.coe LinearMap Complex Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff qExpansion UpperHalfPlane UpperHalfPlane.valueAtInfty	—	qExpansion_coeff Nat.cast_one inv_one iteratedDeriv_zero cuspFunction_apply_zero one_mul

SlashInvariantFormClass

Definitions

Name	Category	Theorems
cuspFunction 📖	CompOp	14 math math: ModularFormClass.hasFPowerSeries_cuspFunction, eq_cuspFunction, ModularFormClass.qExpansion_coeff, ModularFormClass.differentiableAt_cuspFunction, ModularFormClass.hasSum_qExpansion_of_abs_lt, hasFPowerSeriesOnBall_cuspFunction, ModularFormClass.qExpansion_coeff_eq_circleIntegral, ModularForm.cuspFunction_mul, ModularFormClass.hasSum_qExpansion_of_norm_lt, ModularFormClass.cuspFunction_apply_zero, CuspFormClass.cuspFunction_apply_zero, ModularFormClass.analyticAt_cuspFunction_zero, ModularFormClass.differentiableOn_cuspFunction_ball, UpperHalfPlane.IsZeroAtImInfty.cuspFunction_apply_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_cuspFunction 📖	mathematical	Real AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	cuspFunction DFunLike.coe UpperHalfPlane Complex Function.Periodic.qParam UpperHalfPlane.coe	—	UpperHalfPlane.ofComplex_apply Function.Periodic.eq_cuspFunction periodic_comp_ofComplex
periodic_comp_ofComplex 📖	mathematical	Real AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	Function.Periodic Complex Complex.instAdd UpperHalfPlane DFunLike.coe OpenPartialHomeomorph.toFun' UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField UpperHalfPlane.instTopologicalSpace UpperHalfPlane.ofComplex Complex.ofReal	—	add_zero UpperHalfPlane.ofComplex_apply_of_im_pos UpperHalfPlane.ext add_comm SlashInvariantForm.vAdd_apply_of_mem_strictPeriods UpperHalfPlane.ofComplex_apply_of_im_nonpos

UpperHalfPlane

Definitions

Name	Category	Theorems
valueAtInfty 📖	CompOp	5 math math: ModularFormClass.exp_decay_sub_atImInfty, ModularFormClass.qExpansion_coeff_zero, ModularFormClass.cuspFunction_apply_zero, IsZeroAtImInfty.valueAtInfty_eq_zero, ModularFormClass.exp_decay_sub_atImInfty'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
qParam_tendsto_atImInfty 📖	mathematical	Real Real.instLT Real.instZero	Filter.Tendsto UpperHalfPlane Complex Function.Periodic.qParam coe atImInfty nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Complex.instZero	—	Filter.Tendsto.comp Filter.Tendsto.mono_right Function.Periodic.qParam_tendsto nhdsWithin_le_nhds tendsto_coe_atImInfty

UpperHalfPlane.IsZeroAtImInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cuspFunction_apply_zero 📖	mathematical	UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Real Real.instLT Real.instZero	SlashInvariantFormClass.cuspFunction	—	Function.Periodic.cuspFunction_zero_of_zero_at_inf zero_at_infty_comp_ofComplex
exp_decay_atImInfty 📖	mathematical	UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe UpperHalfPlane Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	Asymptotics.IsBigO Complex.instNorm Real.norm UpperHalfPlane.atImInfty Real.exp DivInvMonoid.toDiv Real.instDivInvMonoid Real.instMul Real.instNeg instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.pi UpperHalfPlane.im	—	Nat.instAtLeastTwoHAddOfNat neg_mul valueAtInfty_eq_zero sub_zero ModularFormClass.exp_decay_sub_atImInfty
exp_decay_atImInfty' 📖	mathematical	UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField DFunLike.coe UpperHalfPlane	Real Real.instLT Real.instZero Asymptotics.IsBigO Complex.instNorm Real.norm UpperHalfPlane.atImInfty Real.exp Real.instMul Real.instNeg UpperHalfPlane.im	—	neg_mul valueAtInfty_eq_zero sub_zero ModularFormClass.exp_decay_sub_atImInfty'
valueAtInfty_eq_zero 📖	mathematical	UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	UpperHalfPlane.valueAtInfty	—	Filter.Tendsto.limUnder_eq Complex.instT2Space UpperHalfPlane.instNeBotAtImInfty
zero_at_infty_comp_ofComplex 📖	mathematical	UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	Filter.ZeroAtFilter Filter.comap Real Complex.im Filter.atTop Real.instPreorder UpperHalfPlane OpenPartialHomeomorph.toFun' UpperHalfPlane.instTopologicalSpace UpperHalfPlane.ofComplex	—	Filter.Tendsto.comp UpperHalfPlane.tendsto_comap_im_ofComplex

(root)

Definitions

Name	Category	Theorems
qExpansionAddHom 📖	CompOp	—
qExpansionRingHom 📖	CompOp	1 math math: qExpansionRingHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cuspFunction_add 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction Complex.instZero	Pi.instAdd UpperHalfPlane Complex.instAdd	—	Function.Periodic.cuspFunction_add
cuspFunction_mul 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction Complex.instZero	Pi.instMul UpperHalfPlane Complex.instMul	—	cuspFunction_mul_zero Function.update_of_ne
cuspFunction_mul_zero 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Function.Periodic.cuspFunction Complex.instZero	Pi.instMul Complex.instMul	—	Function.Periodic.cuspFunction.eq_1 Function.update_self Filter.Tendsto.limUnder_eq Complex.instT2Space PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.mul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Function.Periodic.tendsto_nhds_zero
cuspFunction_neg 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction Complex.instZero	Pi.instNeg UpperHalfPlane Complex.instNeg	—	Function.Periodic.cuspFunction_neg
cuspFunction_smul 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction Complex.instZero	Function.hasSMul UpperHalfPlane Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id	—	Function.Periodic.cuspFunction_smul
cuspFunction_sub 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction Complex.instZero	Pi.instSub UpperHalfPlane Complex.instSub	—	Function.Periodic.cuspFunction_sub
hasFPowerSeriesOnBall_cuspFunction 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Function.Periodic.qParam UpperHalfPlane.coe DFunLike.coe UpperHalfPlane SummationFilter.unconditional	HasFPowerSeriesOnBall DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SlashInvariantFormClass.cuspFunction FormalMultilinearSeries.ofScalars Complex.instField Complex.instRing Semifield.toCommSemiring Field.toSemifield IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instZero ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasFPowerSeriesAt.continuousAt HasFPowerSeriesOnBall.hasFPowerSeriesAt AnalyticAt.continuousAt ModularFormClass.analyticAt_cuspFunction_zero ContinuousAt.eventuallyEq_nhds_iff_eventuallyEq_nhdsNE Complex.instT2Space PerfectSpace.not_isolated instPerfectSpace Filter.mp_mem self_mem_nhdsWithin Filter.univ_mem' Function.update_of_ne Function.update_self Filter.EventuallyEq.eq_of_nhds Function.update_eq_self_iff
qExpansionRingHom_apply 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	DFunLike.coe RingHom DirectSum ModularForm AddCommGroup.toAddCommMonoid ModularForm.instAddCommGroup PowerSeries Complex Semiring.toNonAssocSemiring DirectSum.semiring Int.instAddMonoid DirectSum.GRing.toGSemiring DirectSum.GCommRing.toGRing Int.instAddCommMonoid ModularForm.instGCommRing PowerSeries.instSemiring Complex.instSemiring RingHom.instFunLike qExpansionRingHom AddMonoidHom AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoidDirectSum AddMonoidHom.instFunLike DirectSum.of ModularFormClass.qExpansion UpperHalfPlane ModularForm.funLike	—	DirectSum.toSemiring_of qExpansion_one ModularForm.qExpansion_mul
qExpansion_add 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion Pi.instAdd UpperHalfPlane Complex Complex.instAdd DFunLike.coe PowerSeries Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing PowerSeries.instCommRing Complex.commRing	—	PowerSeries.ext
qExpansion_coeff_unique 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods HasSum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Function.Periodic.qParam UpperHalfPlane.coe DFunLike.coe UpperHalfPlane SummationFilter.unconditional	LinearMap RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff ModularFormClass.qExpansion	—	IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasFPowerSeriesOnBall.hasFPowerSeriesAt hasFPowerSeriesOnBall_cuspFunction ModularFormClass.hasFPowerSeries_cuspFunction FormalMultilinearSeries.coeff_ofScalars ModularFormClass.qExpansionFormalMultilinearSeries_coeff IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul HasFPowerSeriesAt.eq_formalMultilinearSeries
qExpansion_eq_zero_iff 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion DFunLike.coe ModularForm UpperHalfPlane Complex ModularForm.funLike PowerSeries PowerSeries.instZero Complex.instZero ModularForm.instZero	—	ModularForm.ext HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional ModularFormClass.hasSum_qExpansion ModularFormClass.modularForm map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MulZeroClass.zero_mul tsum_zero qExpansion_zero
qExpansion_mul 📖	mathematical	AnalyticAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.instNormedAddCommGroup InnerProductSpace.toNormedSpace Complex.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.innerProductSpace SlashInvariantFormClass.cuspFunction Complex.instZero	ModularFormClass.qExpansion Pi.instMul UpperHalfPlane Complex.instMul PowerSeries MvPowerSeries.instMul Complex.instSemiring	—	PowerSeries.ext ModularFormClass.qExpansion_coeff cuspFunction_mul AnalyticAt.continuousAt iteratedDeriv_mul AnalyticAt.contDiffAt Complex.instCompleteSpace Finset.mul_sum PowerSeries.coeff_mul Finset.sum_congr Nat.cast_choose Complex.instCharZero Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul 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.div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ mul_one Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero 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.NF.cons_ne_zero one_ne_zero NeZero.one GroupWithZero.toNontrivial
qExpansion_mul_coeff_zero 📖	mathematical	ContinuousAt Complex UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashInvariantFormClass.cuspFunction Complex.instZero	DFunLike.coe LinearMap Complex.instSemiring RingHom.id Semiring.toNonAssocSemiring PowerSeries PowerSeries.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring PowerSeries.instModule Semiring.toModule LinearMap.instFunLike PowerSeries.coeff ModularFormClass.qExpansion Pi.instMul UpperHalfPlane Complex.instMul	—	ModularFormClass.qExpansion_coeff Nat.cast_one inv_one iteratedDeriv_zero one_mul cuspFunction_mul_zero
qExpansion_neg 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion Pi.instNeg UpperHalfPlane Complex Complex.instNeg DFunLike.coe PowerSeries NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid PowerSeries.instAddCommGroup Complex.addCommGroup	—	neg_smul one_smul qExpansion_smul
qExpansion_of_mul 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion DFunLike.coe ModularForm UpperHalfPlane Complex ModularForm.funLike DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike DirectSum AddCommGroup.toAddCommMonoid ModularForm.instAddCommGroup DirectSum.instMul DirectSum.GSemiring.toGNonUnitalNonAssocSemiring Int.instAddMonoid DirectSum.GRing.toGSemiring DirectSum.GCommRing.toGRing Int.instAddCommMonoid ModularForm.instGCommRing AddMonoidHom instAddCommMonoidDirectSum AddMonoidHom.instFunLike DirectSum.of PowerSeries MvPowerSeries.instMul Complex.instSemiring	—	DirectSum.of_mul_of DirectSum.of_eq_same ModularForm.qExpansion_mul
qExpansion_of_pow 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion DFunLike.coe ModularForm UpperHalfPlane Complex ModularForm.funLike DFinsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DFinsupp.instDFunLike DirectSum AddCommGroup.toAddCommMonoid ModularForm.instAddCommGroup Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero DirectSum.semiring Int.instAddMonoid DirectSum.GRing.toGSemiring DirectSum.GCommRing.toGRing Int.instAddCommMonoid ModularForm.instGCommRing AddMonoidHom instAddCommMonoidDirectSum AddMonoidHom.instFunLike DirectSum.of PowerSeries PowerSeries.instSemiring Complex.instSemiring	—	RingHom.map_pow DirectSum.ofPow DirectSum.of_eq_same qExpansionRingHom_apply
qExpansion_one 📖	mathematical	—	ModularFormClass.qExpansion DFunLike.coe ModularForm UpperHalfPlane Complex ModularForm.funLike ModularForm.instOneOfNatIntOfHasDetPlusMinusOneFinNatReal PowerSeries MvPowerSeries.instOne Complex.instSemiring	—	PowerSeries.ext eq_or_ne Function.update_self Filter.Tendsto.limUnder_eq Complex.instT2Space PerfectSpace.not_isolated instPerfectSpace tendsto_const_nhds Function.Periodic.cuspFunction_eq_of_nonzero iteratedDeriv_const ModularFormClass.qExpansion_coeff mul_ite Nat.cast_one inv_one mul_one MulZeroClass.mul_zero PowerSeries.coeff_one
qExpansion_smul 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion Complex Function.hasSMul UpperHalfPlane Algebra.toSMul Complex.instCommSemiring CommSemiring.toSemiring Algebra.id DFunLike.coe PowerSeries PowerSeries.instSemiring Complex.instSemiring PowerSeries.instAlgebra	—	PowerSeries.ext
qExpansion_sub 📖	mathematical	Real Real.instLT Real.instZero AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Real.instRing SetLike.instMembership AddSubgroup.instSetLike Subgroup.strictPeriods	ModularFormClass.qExpansion Pi.instSub UpperHalfPlane Complex Complex.instSub DFunLike.coe ModularForm ModularForm.funLike PowerSeries SubNegMonoid.toSub AddGroup.toSubNegMonoid PowerSeries.instAddGroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup Complex.instNormedAddCommGroup	—	sub_eq_add_neg qExpansion_neg ModularFormClass.modularForm qExpansion_add
qExpansion_zero 📖	mathematical	—	ModularFormClass.qExpansion Pi.instZero UpperHalfPlane Complex Complex.instZero PowerSeries PowerSeries.instZero	—	Filter.Tendsto.limUnder_eq Complex.instT2Space PerfectSpace.not_isolated instPerfectSpace Filter.Tendsto.mono_left tendsto_const_nhds nhdsWithin_le_nhds PowerSeries.ext ModularFormClass.qExpansion_coeff iteratedDeriv_const_zero MulZeroClass.mul_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass

---

← Back to Index