Documentation Verification Report

Petersson

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

Statistics

Metric	Count
Definitions `petersson`	1
Theorems `norm_petersson_smul`, `petersson_smul`, `of_exp_decay`, `petersson_exp_decay_left`, `petersson_exp_decay_right`, `petersson_isZeroAtImInfty_left`, `petersson_isZeroAtImInfty_right`, `petersson_continuous`, `petersson_norm_symm`, `petersson_slash`, `petersson_slash_SL`, `petersson_symm`	12
Total	13

SlashInvariantFormClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_petersson_smul` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`Norm.norm` `Complex` `Complex.instNorm` `UpperHalfPlane.petersson` `DFunLike.coe` `UpperHalfPlane` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `UpperHalfPlane.glAction`	—	`slash_action_eq` `UpperHalfPlane.petersson_slash` `Subgroup.HasDetPlusMinusOne.abs_det` `Real.instIsOrderedRing` `Complex.ofReal_one` `one_zpow` `one_mul` `UpperHalfPlane.norm_σ`
`petersson_smul` 📖	mathematical	`Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Subgroup` `Units.instGroup` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `SetLike.instMembership` `Subgroup.instSetLike`	`UpperHalfPlane.petersson` `DFunLike.coe` `UpperHalfPlane` `Complex` `SemigroupAction.toSMul` `Monoid.toSemigroup` `Units.instMonoid` `MulAction.toSemigroupAction` `UpperHalfPlane.glAction`	—	`Subgroup.HasDetOne.det_eq` `abs_one` `Real.instIsOrderedRing` `one_zpow` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `one_mul` `slash_action_eq` `UpperHalfPlane.petersson_slash`

UpperHalfPlane

Definitions

Name	Category	Theorems
`petersson` 📖	CompOp	14 math math: `CuspFormClass.petersson_bounded_left`, `IsZeroAtImInfty.petersson_exp_decay_left`, `ModularFormClass.exists_petersson_le`, `CuspFormClass.petersson_bounded_right`, `petersson_continuous`, `petersson_norm_symm`, `IsZeroAtImInfty.petersson_isZeroAtImInfty_left`, `petersson_symm`, `petersson_slash_SL`, `SlashInvariantFormClass.norm_petersson_smul`, `SlashInvariantFormClass.petersson_smul`, `IsZeroAtImInfty.petersson_exp_decay_right`, `IsZeroAtImInfty.petersson_isZeroAtImInfty_right`, `petersson_slash`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`petersson_continuous` 📖	mathematical	`Continuous` `UpperHalfPlane` `Complex` `instTopologicalSpace` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField`	`petersson`	—	`Continuous.comp'` `continuous_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `Continuous.prodMk` `Complex.continuous_conj` `Continuous.zpow₀` `IsTopologicalDivisionRing.toContinuousInv₀` `Complex.continuous_ofReal` `continuous_im` `im_ne_zero`
`petersson_norm_symm` 📖	mathematical	—	`Norm.norm` `Complex` `Complex.instNorm` `petersson`	—	`petersson_symm` `RCLike.norm_conj`
`petersson_slash` 📖	mathematical	—	`petersson` `SlashAction.map` `Matrix.GeneralLinearGroup` `Real` `Fin.fintype` `Real.semiring` `Units.instMonoid` `Matrix` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Matrix.semiring` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.instSlashActionIntGeneralLinearGroupFinOfNatNatRealForallUpperHalfPlaneComplex` `Complex.instMul` `DivInvMonoid.toZPow` `Complex.instDivInvMonoid` `Complex.ofReal` `abs` `Real.lattice` `Real.instAddGroup` `Units.val` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `DFunLike.coe` `MonoidHom` `Units` `MulOneClass.toMulOne` `Units.instMulOneClass` `MonoidHom.instFunLike` `Matrix.GeneralLinearGroup.det` `RingHom` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `RingHom.instFunLike` `σ` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `glAction`	—	`Nat.cast_zero` `abs_ne_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Matrix.GeneralLinearGroup.det_ne_zero` `Real.instNontrivial` `zpow_neg` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_zpow₀` `RingHomClass.toMonoidWithZeroHomClass` `Complex.conj_ofReal` `map_inv₀` `Mathlib.Tactic.Abel.subst_into_addg` `Mathlib.Tactic.Abel.unfold_sub` `Mathlib.Tactic.Abel.term_atomg` `Mathlib.Tactic.Abel.subst_into_negg` `Mathlib.Tactic.Abel.term_neg` `neg_zero` `Mathlib.Tactic.Abel.term_add_constg` `zero_add` `Mathlib.Tactic.Abel.term_add_termg` `Mathlib.Meta.NormNum.IsNat.to_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.isNat_ofNat` `add_zero` `Mathlib.Meta.NormNum.IsInt.neg_to_eq` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.isInt_neg` `Mathlib.Meta.NormNum.IsNat.to_isInt` `zpow_add₀` `Complex.normSq_eq_conj_mul_self` `mul_zpow` `mul_inv_rev` `Mathlib.Tactic.Ring.of_eq` `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.inv_congr` `Mathlib.Tactic.Ring.inv_single` `Mathlib.Tactic.Ring.inv_mul` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.IsNNRat.to_isNat` `Mathlib.Meta.NormNum.isNNRat_inv_pos` `Complex.instCharZero` `Mathlib.Meta.NormNum.IsNat.to_isNNRat` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `div_zpow` `div_eq_mul_inv` `im_smul_eq_div_normSq` `Complex.ofReal_div` `Complex.ofReal_mul` `σ_conj` `σ_ofReal`
`petersson_slash_SL` 📖	mathematical	—	`petersson` `SlashAction.map` `Matrix.SpecialLinearGroup` `Fin.fintype` `Int.instCommRing` `Matrix.SpecialLinearGroup.monoid` `Pi.addMonoid` `UpperHalfPlane` `Complex` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Complex.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `ModularForm.SLAction` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `SLAction` `Ring.toIntAlgebra` `Real` `Real.instRing`	—	`petersson_slash` `Matrix.SpecialLinearGroup.coeToGL_det` `abs_one` `Real.instIsOrderedRing` `one_zpow` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `one_mul`
`petersson_symm` 📖	mathematical	—	`petersson` `DFunLike.coe` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Complex.instCommSemiring` `RingHom.instFunLike` `starRingEnd` `Complex.instStarRing`	—	`mul_comm` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_zpow₀` `RingHomClass.toMonoidWithZeroHomClass` `Complex.conj_ofReal` `RingHomCompTriple.comp_apply` `RingHomInvPair.triples₂` `RingHomInvPair.instStarRingEnd`

UpperHalfPlane.IsZeroAtImInfty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`of_exp_decay` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Asymptotics.IsBigO` `UpperHalfPlane` `NormedAddCommGroup.toNorm` `Real.norm` `UpperHalfPlane.atImInfty` `Real.exp` `Real.instMul` `Real.instNeg` `UpperHalfPlane.im`	`UpperHalfPlane.IsZeroAtImInfty` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	—	`Asymptotics.IsBigO.trans_tendsto` `Filter.Tendsto.comp` `Real.tendsto_exp_atBot` `Filter.Tendsto.const_mul_atTop_of_neg` `Real.instIsStrictOrderedRing` `neg_lt_zero` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Filter.tendsto_id` `Filter.tendsto_comap`
`petersson_exp_decay_left` 📖	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` `UpperHalfPlane.petersson` `Real.exp` `Real.instMul` `Real.instNeg` `UpperHalfPlane.im`	—	`exp_decay_atImInfty'` `exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Asymptotics.IsBigO.of_norm_left` `norm_mul` `NormedDivisionRing.toNormMulClass` `Complex.norm_conj` `mul_comm` `norm_zpow` `mul_assoc` `Complex.norm_real` `Real.norm_of_nonneg` `LT.lt.le` `UpperHalfPlane.im_pos` `one_mul` `ModularFormClass.bdd_at_infty` `Asymptotics.IsBigO.mul` `Asymptotics.IsBigO.norm_left` `Asymptotics.IsBigO.trans` `Asymptotics.isBigO_refl` `Asymptotics.IsBigO.comp_tendsto` `neg_mul` `Real.rpow_intCast` `Asymptotics.IsLittleO.isBigO` `isLittleO_exp_mul_rpow_of_lt` `neg_lt_neg` `Real.instIsOrderedAddMonoid` `Filter.tendsto_comap`
`petersson_exp_decay_right` 📖	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` `UpperHalfPlane.petersson` `Real.exp` `Real.instMul` `Real.instNeg` `UpperHalfPlane.im`	—	`petersson_exp_decay_left` `Asymptotics.IsBigO.of_norm_left` `Asymptotics.IsBigO.congr_left` `Asymptotics.IsBigO.norm_left` `UpperHalfPlane.petersson_norm_symm`
`petersson_isZeroAtImInfty_left` 📖	mathematical	`UpperHalfPlane.IsZeroAtImInfty` `Complex` `Complex.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `DFunLike.coe` `UpperHalfPlane`	`UpperHalfPlane.petersson`	—	`of_exp_decay` `petersson_exp_decay_left`
`petersson_isZeroAtImInfty_right` 📖	mathematical	`UpperHalfPlane.IsZeroAtImInfty` `Complex` `Complex.instZero` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `DFunLike.coe` `UpperHalfPlane`	`UpperHalfPlane.petersson`	—	`of_exp_decay` `petersson_exp_decay_right`

---

← Back to Index