Documentation Verification Report

Bounds

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

Statistics

Metric	Count
Definitions	0
Theorems `exists_bound`, `petersson_bounded_left`, `petersson_bounded_right`, `qExpansion_isBigO`, `exists_bound`, `exists_petersson_le`, `qExpansion_isBigO`, `exists_bound_fundamental_domain_of_isBigO`, `exists_bound_of_invariant`, `exists_bound_of_invariant_of_isBigO`, `exists_bound_of_subgroup_invariant`, `exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO`, `exists_bound_of_subgroup_invariant_of_isBigO`, `qExpansion_coeff_isBigO_of_norm_isBigO`	14
Total	14

CuspFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_bound` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `DFunLike.coe` `UpperHalfPlane` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instPow` `UpperHalfPlane.im` `Real.instIntCast` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `petersson_bounded_left` `CuspForm.instModularFormClassOfCuspFormClass` `sq_le_sq₀` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `norm_nonneg` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `Real.sqrt_nonneg` `Real.rpow_pos_of_pos` `UpperHalfPlane.im_pos` `div_pow` `Real.sq_sqrt` `LE.le.trans` `le_imp_le_of_le_of_le` `le_refl` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `UpperHalfPlane.petersson.eq_1` `Real.rpow_mul_natCast` `LT.lt.le` `Complex.norm_mul` `RCLike.norm_conj` `norm_zpow` `Complex.norm_real` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `IsUnit.div_mul_cancel` `RCLike.charZero_rclike` `Real.rpow_intCast` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `zpow_pos` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.one` `GroupWithZero.toNontrivial`
`petersson_bounded_left` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `UpperHalfPlane.petersson` `DFunLike.coe` `UpperHalfPlane`	—	`norm_norm` `ModularGroup.exists_bound_of_subgroup_invariant` `Continuous.norm` `UpperHalfPlane.petersson_continuous` `ModularFormClass.continuous` `CuspForm.instModularFormClassOfCuspFormClass` `UpperHalfPlane.IsZeroAtImInfty.isBoundedAtImInfty` `UpperHalfPlane.IsZeroAtImInfty.eq_1` `Filter.ZeroAtFilter.eq_1` `tendsto_zero_iff_norm_tendsto_zero` `map_inv` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `RCLike.charZero_rclike` `MonoidHom.instMonoidHomClass` `Matrix.SpecialLinearGroup.map_mapGL` `AddCommGroup.intIsScalarTower` `Subgroup.IsArithmetic.conj` `UpperHalfPlane.IsZeroAtImInfty.petersson_isZeroAtImInfty_left` `instFactIsCuspInftyRealOfIsArithmetic` `Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic` `Subgroup.IsArithmetic.discreteTopology` `cuspForm` `ModularFormClass.modularForm` `zero_at_infty` `SlashInvariantFormClass.norm_petersson_smul` `toSlashInvariantFormClass` `ModularFormClass.toSlashInvariantFormClass`
`petersson_bounded_right` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `UpperHalfPlane.petersson` `DFunLike.coe` `UpperHalfPlane`	—	`UpperHalfPlane.petersson_norm_symm` `petersson_bounded_left`
`qExpansion_isBigO` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `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` `Subgroup.strictWidthInfty` `UpperHalfPlane` `Real.instPow` `Real.instNatCast` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instIntCast` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`qExpansion_coeff_isBigO_of_norm_isBigO` `CuspForm.instModularFormClassOfCuspFormClass` `Nat.instAtLeastTwoHAddOfNat` `exists_bound` `Asymptotics.isBigO_of_le'` `LE.le.trans` `of_eq` `instReflLe` `Real.norm_of_nonneg` `le_of_lt` `Real.rpow_pos_of_pos` `UpperHalfPlane.im_pos` `Real.rpow_neg` `LT.lt.le` `div_eq_mul_inv`

ModularFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_bound` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `DFunLike.coe` `UpperHalfPlane` `Real.instMul` `Real.instMax` `Real.instOne` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `DivInvMonoid.toZPow` `UpperHalfPlane.im`	—	`exists_petersson_le` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `le_trans` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `norm_nonneg` `zpow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `lt_max_of_lt_left` `UpperHalfPlane.im_pos` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Nat.cast_zero` `zpow_natCast` `Complex.norm_real` `norm_pos_iff` `pow_ne_zero` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `UpperHalfPlane.im_ne_zero` `sq_le_sq₀` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.sqrt_nonneg` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `mul_pow` `Real.sq_sqrt` `LE.le.trans` `mul_div_assoc` `le_div_iff₀` `sq` `Complex.norm_conj` `norm_mul` `UpperHalfPlane.petersson.eq_1` `Eq.le` `NNReal.canLift` `LT.lt.le` `coe_nnnorm` `Complex.nnnorm_real` `Monotone.map_max` `pow_left_mono` `NNReal.mulLeftMono` `covariant_swap_mul_of_covariant_mul` `max_div_div_right` `NNReal.instIsStrictOrderedRing` `zero_le` `NNReal.instCanonicallyOrderedAdd` `nnnorm_pow` `NormedDivisionRing.to_normOneClass` `NNReal.nnnorm_eq` `div_self` `NNReal.instNoZeroDivisors` `LT.lt.ne'` `one_pow` `one_div` `inv_pow` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_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.one_div_eq_eval` `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.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `pow_pos` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial`
`exists_petersson_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `UpperHalfPlane.petersson` `DFunLike.coe` `UpperHalfPlane` `Real.instMul` `DivInvMonoid.toZPow` `Real.instDivInvMonoid` `Real.instMax` `UpperHalfPlane.im` `DivInvMonoid.toDiv` `Real.instOne`	—	`norm_norm` `Nat.cast_one` `Real.rpow_intCast` `ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO` `Continuous.norm` `UpperHalfPlane.petersson_continuous` `continuous` `Nat.cast_zero` `Int.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Complex.norm_mul` `RCLike.norm_conj` `norm_zpow` `Complex.norm_real` `Real.norm_of_nonneg` `LT.lt.le` `UpperHalfPlane.im_pos` `mul_one` `one_mul` `Asymptotics.IsBigO.mul` `NormedDivisionRing.toNormMulClass` `Asymptotics.IsBigO.norm_left` `bdd_at_infty_slash` `Asymptotics.isBigO_refl` `SlashInvariantFormClass.norm_petersson_smul` `Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic` `toSlashInvariantFormClass`
`qExpansion_isBigO` 📖	mathematical	—	`Asymptotics.IsBigO` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.atTop` `Nat.instPreorder` `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` `Subgroup.strictWidthInfty` `UpperHalfPlane` `DivInvMonoid.toZPow` `Real.instDivInvMonoid` `Real.instNatCast`	—	`qExpansion_coeff_isBigO_of_norm_isBigO` `exists_bound` `Asymptotics.IsBigO_def` `Real.rpow_intCast` `Asymptotics.IsBigOWith_def` `Filter.mp_mem` `eventually_le_nhds` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Filter.univ_mem'` `LE.le.trans` `le_of_eq` `max_eq_right` `one_le_one_div` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `zpow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `UpperHalfPlane.im_pos` `zpow_le_one₀` `zpow_neg` `Real.norm_of_nonneg` `le_of_lt` `inv_pos_of_pos` `one_div`

ModularGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_bound_fundamental_domain_of_isBigO` 📖	mathematical	`Continuous` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Asymptotics.IsBigO` `Real` `SeminormedAddCommGroup.toNorm` `Real.norm` `UpperHalfPlane.atImInfty` `Real.instPow` `UpperHalfPlane.im`	`Real.instLE` `Norm.norm` `Real.instMul`	—	`Asymptotics.IsBigO.exists_pos` `Filter.eventually_atTop` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.eventually_comap` `UpperHalfPlane.atImInfty.eq_1` `Asymptotics.IsBigOWith_def` `Continuous.continuousOn` `Continuous.div` `IsTopologicalDivisionRing.toContinuousInv₀` `instIsTopologicalDivisionRingReal` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.norm` `Continuous.rpow_const` `UpperHalfPlane.continuous_im` `UpperHalfPlane.im_ne_zero` `ne_of_gt` `Real.rpow_pos_of_pos` `UpperHalfPlane.im_pos` `norm_div` `abs_norm` `Real.norm_rpow_of_nonneg` `LT.lt.le` `Real.norm_of_nonneg` `IsCompact.exists_bound_of_continuousOn` `isCompact_truncatedFundamentalDomain` `le_total` `LE.le.trans` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_max_left` `le_of_lt` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `le_max_right`
`exists_bound_of_invariant` 📖	mathematical	`Continuous` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `UpperHalfPlane.IsBoundedAtImInfty` `SeminormedAddCommGroup.toNorm` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing`	`Real.instLE` `Norm.norm`	—	`one_div` `Real.rpow_zero` `mul_one` `exists_bound_of_invariant_of_isBigO` `le_rfl`
`exists_bound_of_invariant_of_isBigO` 📖	mathematical	`Continuous` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero` `Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `Real.norm` `UpperHalfPlane.atImInfty` `Real.instPow` `UpperHalfPlane.im` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing`	`Norm.norm` `Real.instMul` `Real.instMax` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`exists_bound_fundamental_domain_of_isBigO` `exists_smul_mem_fd` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Real.rpow_le_rpow` `le_of_lt` `UpperHalfPlane.im_pos` `im_smul_eq_div_normSq` `denom_apply` `zero_ne_one` `Matrix.det_fin_two` `MulZeroClass.mul_zero` `sub_zero` `Matrix.SpecialLinearGroup.det_coe` `Nat.cast_one` `Int.cast_one` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `one_le_sq_iff_one_le_abs` `Int.instIsStrictOrderedRing` `Int.one_le_abs` `le_trans` `Int.cast_zero` `MulZeroClass.zero_mul` `zero_add` `Complex.normSq_intCast` `sq` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.pow_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_ofNat` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `PosMulReflectLE.toPosMulReflectLT` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `one_div` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `inv_le_one_of_one_le₀` `le_max_left` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `ne_of_gt` `one_ne_zero` `div_le_div₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `add_zero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.add_pf_add_overlap` `Mathlib.Tactic.Ring.add_overlap_pf` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.pow_nat` `Mathlib.Tactic.Ring.coeff_one` `Mathlib.Tactic.Ring.pow_one_cast` `Mathlib.Tactic.Ring.pow_bit0` `Mathlib.Tactic.Ring.pow_one` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.mul_one` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.add_lt_of_le_of_neg` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `sq_nonneg` `AddGroup.existsAddOfLE` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `mul_nonneg_of_nonpos_of_nonpos` `IsOrderedRing.toMulPosMono` `covariant_swap_add_of_covariant_add` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `le_max_right` `Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos` `norm_nonneg` `Real.rpow_pos_of_pos` `div_le_iff₀`
`exists_bound_of_subgroup_invariant` 📖	mathematical	`Continuous` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `UpperHalfPlane.IsBoundedAtImInfty` `SeminormedAddCommGroup.toNorm` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing` `Matrix.GeneralLinearGroup` `Real.semiring` `Units.instMonoid` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `UpperHalfPlane.glAction`	`Real.instLE` `Norm.norm`	—	`one_div` `Real.rpow_zero` `mul_one` `exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO` `le_rfl`
`exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO` 📖	mathematical	`Continuous` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero` `Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `Real.norm` `UpperHalfPlane.atImInfty` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing` `Real.instPow` `UpperHalfPlane.im` `Matrix.GeneralLinearGroup` `Real.semiring` `Units.instMonoid` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `UpperHalfPlane.glAction`	`Norm.norm` `Real.instMul` `Real.instMax` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`exists_bound_of_subgroup_invariant_of_isBigO` `Subgroup.IsArithmetic.finiteIndex_comap`
`exists_bound_of_subgroup_invariant_of_isBigO` 📖	mathematical	`Continuous` `UpperHalfPlane` `UpperHalfPlane.instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `Real` `Real.instLE` `Real.instZero` `Asymptotics.IsBigO` `SeminormedAddCommGroup.toNorm` `Real.norm` `UpperHalfPlane.atImInfty` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Matrix.SpecialLinearGroup.monoid` `MulAction.toSemigroupAction` `UpperHalfPlane.SLAction` `Ring.toIntAlgebra` `Real.instRing` `Real.instPow` `UpperHalfPlane.im`	`Norm.norm` `Real.instMul` `Real.instMax` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Real.instOne`	—	`QuotientGroup.leftRel_apply` `Quotient.eq` `Quotient.eq_iff_equiv` `mul_inv_cancel_left` `mul_inv_rev` `SemigroupAction.mul_smul` `InvMemClass.inv_mem` `SubgroupClass.toInvMemClass` `Subgroup.instSubgroupClass` `QuotientGroup.induction_on` `Continuous.comp'` `Continuous.const_smul` `UpperHalfPlane.instContinuousGLSMul` `continuous_id'` `MulAction.left_quotientAction` `inv_smul_smul` `Quot.induction_on` `exists_bound_of_invariant_of_isBigO` `continuous_finset_sum` `IsTopologicalSemiring.toContinuousAdd` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Continuous.norm` `Asymptotics.IsBigO.sum` `Asymptotics.IsBigO.norm_left` `Fintype.sum_equiv` `le_trans` `Finset.sum_congr` `Real.norm_of_nonneg` `Finset.sum_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `norm_nonneg` `inv_one` `one_smul` `Finset.single_le_sum` `Finset.mem_univ`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`qExpansion_coeff_isBigO_of_norm_isBigO` 📖	mathematical	`Asymptotics.IsBigO` `UpperHalfPlane` `Complex` `Real` `Complex.instNorm` `Real.norm` `Filter.comap` `UpperHalfPlane.im` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instZero` `DFunLike.coe` `Real.instPow` `Real.instNeg`	`Filter.atTop` `Nat.instPreorder` `LinearMap` `Complex.instSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `PowerSeries` `PowerSeries.instAddCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `PowerSeries.instModule` `Semiring.toModule` `LinearMap.instFunLike` `PowerSeries.coeff` `ModularFormClass.qExpansion` `Subgroup.strictWidthInfty` `Real.instNatCast`	—	`Subgroup.strictWidthInfty_pos_iff` `Subgroup.instDiscreteTopStrictPeriods` `instIsTopologicalRingReal` `Subgroup.IsArithmetic.discreteTopology` `Subgroup.instHasDetPlusMinusOneFinOfNatNatRealOfIsArithmetic` `Fact.out` `instFactIsCuspInftyRealOfIsArithmetic` `LT.lt.ne'` `Subgroup.strictWidthInfty_mem_strictPeriods` `Asymptotics.IsBigO.exists_pos` `Asymptotics.isBigO_iff` `Nat.instAtLeastTwoHAddOfNat` `Filter.mp_mem` `Filter.Tendsto.eventually` `Filter.Tendsto.comp` `tendsto_inv_atTop_zero` `Real.instIsStrictOrderedRing` `instOrderTopologyReal` `tendsto_natCast_atTop_atTop` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.eventually_comap` `Asymptotics.IsBigOWith_def` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.univ_mem'` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `ModularFormClass.qExpansion_coeff_eq_intervalIntegral` `intervalIntegral.integral_const_mul` `Complex.ofReal_div` `LE.le.trans` `intervalIntegral.norm_integral_le_integral_norm` `le_of_lt` `one_div` `Complex.inv_re` `Complex.normSq_natCast` `div_self_mul_self'` `mul_one` `Complex.inv_im` `neg_zero` `zero_div` `MulZeroClass.mul_zero` `add_zero` `zero_add` `Real.norm_of_nonneg` `Real.rpow_pos_of_pos` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_div` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `Complex.norm_real` `norm_pow` `mul_assoc` `LT.lt.le` `Function.Periodic.norm_qParam` `Real.exp_nat_mul` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `mul_le_mul` `IsOrderedRing.toMulPosMono` `div_le_div₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `le_refl` `Real.exp_pos` `Real.exp_monotone` `neg_mul` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `neg_div` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `one_mul` `mul_neg` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.inv_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_pos` `Real.pi_pos` `Mathlib.Meta.NormNum.instAtLeastTwo` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `le_imp_le_of_le_of_le` `Real.rpow_neg_eq_inv_rpow` `inv_inv` `norm_nonneg` `intervalIntegral.integral_mono` `Continuous.intervalIntegrable` `Real.locallyFinite_volume` `Continuous.norm` `Continuous.comp'` `continuous_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.prodMk` `continuous_const` `continuous_id'` `Continuous.div₀` `IsTopologicalDivisionRing.toContinuousInv₀` `Continuous.pow` `Function.Periodic.continuous_qParam` `Continuous.fun_add` `IsTopologicalSemiring.toContinuousAdd` `Complex.continuous_ofReal` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `Complex.instNontrivial` `ModularFormClass.continuous` `Continuous.upperHalfPlaneMk` `le_of_eq` `intervalIntegral.integral_const` `Real.instCompleteSpace` `sub_zero` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `one_ne_zero`

---

← Back to Index