Documentation Verification Report

IsBoundedAtImInfty

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

Statistics

Metric	Count
Definitions `IsBoundedAtImInfty`	1
Theorems `isBoundedAtImInfty_eisensteinSeriesSIF`, `isBoundedAtImInfty_eisensteinSeries_SIF`, `norm_le_tsum_norm`, `summable_norm_eisSummand`	4
Total	5

EisensteinSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isBoundedAtImInfty_eisensteinSeriesSIF` 📖	mathematical	—	`UpperHalfPlane.IsBoundedAtImInfty` `Complex` `Complex.instNorm` `SlashAction.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `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` `DFunLike.coe` `SlashInvariantForm` `Subgroup.map` `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` `SlashInvariantForm.funLike` `eisensteinSeriesSIF`	—	`Nat.instAtLeastTwoHAddOfNat` `Nat.ofNat_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip` `NeZero.pos` `Nat.instCanonicallyOrderedAdd` `eisensteinSeries_slash_apply` `eisensteinSeriesSIF_apply` `SlashInvariantForm.T_zpow_width_invariant` `le_trans` `norm_le_tsum_norm` `Int.cast_ofNat` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Summable.tsum_le_tsum` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `SummationFilter.instNeBotUnconditional` `norm_zpow` `two_pos` `Real.rpow_intCast` `summand_bound_of_mem_verticalStrip` `LT.lt.le` `lt_trans` `UpperHalfPlane.verticalStrip_anti_right` `summable_norm_eisSummand` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_one_div_norm_rpow`
`isBoundedAtImInfty_eisensteinSeries_SIF` 📖	mathematical	—	`UpperHalfPlane.IsBoundedAtImInfty` `Complex` `Complex.instNorm` `SlashAction.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `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` `DFunLike.coe` `SlashInvariantForm` `Subgroup.map` `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` `SlashInvariantForm.funLike` `eisensteinSeriesSIF`	—	`isBoundedAtImInfty_eisensteinSeriesSIF`
`norm_le_tsum_norm` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `eisensteinSeries` `tsum` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `eisSummand` `SummationFilter.unconditional`	—	`le_trans` `norm_tsum_le_tsum_norm` `Summable.subtype` `instIsUniformAddGroupReal` `Real.instCompleteSpace` `summable_norm_eisSummand` `Summable.tsum_subtype_le` `Real.instIsOrderedAddMonoid` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `norm_nonneg`
`summable_norm_eisSummand` 📖	mathematical	—	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Norm.norm` `Complex` `Complex.instNorm` `eisSummand` `SummationFilter.unconditional`	—	`Nat.instAtLeastTwoHAddOfNat` `Int.cast_ofNat` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Summable.of_nonneg_of_le` `norm_nonneg` `Summable.mul_left` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `summable_one_div_norm_rpow` `norm_zpow` `Real.rpow_intCast` `summand_bound` `le_of_lt` `Int.cast_pos` `IsOrderedRing.toIsOrderedAddMonoid` `Real.instIsOrderedRing` `IsOrderedRing.toZeroLEOneClass` `NeZero.one` `Real.instNontrivial` `lt_of_lt_of_le` `Mathlib.Meta.Positivity.pos_of_isNat` `IsStrictOrderedRing.toIsOrderedRing` `Int.instIsStrictOrderedRing` `Int.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat`

UpperHalfPlane

Definitions

Name	Category	Theorems
`IsBoundedAtImInfty` 📖	MathDef	11 math math: `OnePoint.isBoundedAt_iff_exists_SL2Z`, `OnePoint.isBoundedAt_iff_forall_SL2Z`, `isBoundedAtImInfty_iff`, `zero_form_isBoundedAtImInfty`, `OnePoint.isBoundedAt_iff`, `OnePoint.isBoundedAt_infty_iff`, `ModularFormClass.bdd_at_infty`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF`, `IsZeroAtImInfty.isBoundedAtImInfty`, `ModularFormClass.bdd_at_infty_slash`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF`

---

← Back to Index