BoundedAtCusp

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

Statistics

Metric	Count
Definitions IsBoundedAt, IsZeroAt	2
Theorems add, smul_iff, add, smul_iff, isBoundedAt_iff, isBoundedAt_iff_exists_SL2Z, isBoundedAt_iff_forall_SL2Z, isBoundedAt_infty_iff, isZeroAt_iff, isZeroAt_iff_exists_SL2Z, isZeroAt_iff_forall_SL2Z, isZeroAt_infty_iff, slash, slash	14
Total	16

OnePoint

Definitions

Name	Category	Theorems
IsBoundedAt 📖	MathDef	7 math math: isBoundedAt_iff_exists_SL2Z, isBoundedAt_iff_forall_SL2Z, isBoundedAt_iff, isBoundedAt_infty_iff, IsBoundedAt.smul_iff, ModularFormClass.bdd_at_cusps, ModularForm.bdd_at_cusps'
IsZeroAt 📖	MathDef	7 math math: CuspFormClass.zero_at_cusps, isZeroAt_iff_exists_SL2Z, isZeroAt_infty_iff, isZeroAt_iff_forall_SL2Z, IsZeroAt.smul_iff, CuspForm.zero_at_cusps', isZeroAt_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isBoundedAt_iff 📖	mathematical	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction Real.instField Real.decidableEq infty	IsBoundedAt UpperHalfPlane.IsBoundedAtImInfty Complex Complex.instNorm SlashAction.map Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	—
isBoundedAt_iff_exists_SL2Z 📖	mathematical	IsCusp MonoidHom.range 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	IsBoundedAt CommSemiring.toSemiring CommRing.toCommSemiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction instGLAction Real.instField Real.decidableEq DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike infty UpperHalfPlane.IsBoundedAtImInfty Complex Complex.instNorm SlashAction.map Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction	—	isCusp_SL2Z_iff'
isBoundedAt_iff_forall_SL2Z 📖	mathematical	IsCusp MonoidHom.range 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	IsBoundedAt UpperHalfPlane.IsBoundedAtImInfty Complex Complex.instNorm SlashAction.map Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction	—	isCusp_SL2Z_iff'
isBoundedAt_infty_iff 📖	mathematical	—	IsBoundedAt infty Real UpperHalfPlane.IsBoundedAtImInfty Complex Complex.instNorm	—	SlashAction.slash_one one_smul UpperHalfPlane.IsBoundedAtImInfty.slash smul_infty_eq_self_iff
isZeroAt_iff 📖	mathematical	Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction instGLAction Real.instField Real.decidableEq infty	IsZeroAt UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashAction.map Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	—
isZeroAt_iff_exists_SL2Z 📖	mathematical	IsCusp MonoidHom.range 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	IsZeroAt CommSemiring.toSemiring CommRing.toCommSemiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid MulAction.toSemigroupAction instGLAction Real.instField Real.decidableEq DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass Matrix.SpecialLinearGroup.monoid Units.instMulOneClass MonoidHom.instFunLike infty UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashAction.map Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction	—	isCusp_SL2Z_iff'
isZeroAt_iff_forall_SL2Z 📖	mathematical	IsCusp MonoidHom.range 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	IsZeroAt UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField SlashAction.map Matrix.SpecialLinearGroup.monoid Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.SLAction	—	isCusp_SL2Z_iff'
isZeroAt_infty_iff 📖	mathematical	—	IsZeroAt infty Real UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	SlashAction.slash_one one_smul UpperHalfPlane.IsZeroAtImInfty.slash smul_infty_eq_self_iff

OnePoint.IsBoundedAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	OnePoint.IsBoundedAt	Pi.instAdd UpperHalfPlane Complex Complex.instAdd	—	SlashAction.add_slash Filter.BoundedAtFilter.add
smul_iff 📖	mathematical	—	OnePoint.IsBoundedAt Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction OnePoint.instGLAction Real.instField Real.decidableEq SlashAction.map Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	eq_1 Equiv.forall_congr_left Equiv.mulLeft_symm inv_inv SemigroupAction.mul_smul

OnePoint.IsZeroAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	OnePoint.IsZeroAt	Pi.instAdd UpperHalfPlane Complex Complex.instAdd	—	SlashAction.add_slash Filter.ZeroAtFilter.add IsTopologicalSemiring.toContinuousAdd IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing
smul_iff 📖	mathematical	—	OnePoint.IsZeroAt Matrix.GeneralLinearGroup Real Fin.fintype Real.semiring OnePoint SemigroupAction.toSMul Monoid.toSemigroup Units.instMonoid Matrix MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring MulAction.toSemigroupAction OnePoint.instGLAction Real.instField Real.decidableEq SlashAction.map Pi.addMonoid UpperHalfPlane Complex ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	eq_1 Equiv.forall_congr_left Equiv.mulLeft_symm inv_inv SemigroupAction.mul_smul

UpperHalfPlane.IsBoundedAtImInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slash 📖	mathematical	Units.val Matrix Real MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring Fin.fintype Real.instZero UpperHalfPlane.IsBoundedAtImInfty Complex Complex.instNorm	SlashAction.map Matrix.GeneralLinearGroup Units.instMonoid Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	eq_1 Filter.BoundedAtFilter.eq_1 Asymptotics.isBigO_norm_left Asymptotics.IsBigO.const_mul_left Asymptotics.IsBigO.comp_tendsto UpperHalfPlane.tendsto_smul_atImInfty MulZeroClass.zero_mul zero_add zpow_neg mul_assoc Complex.norm_mul UpperHalfPlane.norm_σ norm_zpow Complex.norm_real abs_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add norm_inv mul_comm

UpperHalfPlane.IsZeroAtImInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
slash 📖	mathematical	Units.val Matrix Real MonoidWithZero.toMonoid Semiring.toMonoidWithZero Matrix.semiring Real.semiring Fin.fintype Real.instZero UpperHalfPlane.IsZeroAtImInfty Complex Complex.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	SlashAction.map Matrix.GeneralLinearGroup Units.instMonoid Pi.addMonoid UpperHalfPlane ESeminormedAddMonoid.toAddMonoid SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup Complex.instNormedAddCommGroup ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex	—	eq_1 Filter.ZeroAtFilter.eq_1 tendsto_zero_iff_norm_tendsto_zero MulZeroClass.zero_mul zero_add zpow_neg mul_assoc Complex.norm_mul UpperHalfPlane.norm_σ norm_zpow Complex.norm_real abs_abs IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add norm_inv Filter.Tendsto.mul_const IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal Filter.Tendsto.comp UpperHalfPlane.tendsto_smul_atImInfty

---

← Back to Index