Commit 2025-09-16 15:34 36939570

View on Github →

feat(NumberTheory/ModularForms): define boundedness / vanishing at a cusp (#29560)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

added theorem UpperHalfPlane.tendsto_smul_atImInfty

Modified Mathlib/Analysis/Complex/UpperHalfPlane/MoebiusAction.lean

added theorem UpperHalfPlane.norm_σ

deleted def UpperHalfPlane.σ

Created Mathlib/NumberTheory/ModularForms/BoundedAtCusp.lean

added theorem OnePoint.IsBoundedAt.add

added theorem OnePoint.IsBoundedAt.smul_iff

added def OnePoint.IsBoundedAt

added theorem OnePoint.IsZeroAt.add

added theorem OnePoint.IsZeroAt.smul_iff

added def OnePoint.IsZeroAt

added theorem OnePoint.isBoundedAt_iff

added theorem OnePoint.isBoundedAt_iff_exists_SL2Z

added theorem OnePoint.isBoundedAt_iff_forall_SL2Z

added theorem OnePoint.isBoundedAt_infty_iff

added theorem OnePoint.isZeroAt_iff

added theorem OnePoint.isZeroAt_iff_exists_SL2Z

added theorem OnePoint.isZeroAt_iff_forall_SL2Z

added theorem OnePoint.isZeroAt_infty_iff

added theorem UpperHalfPlane.IsBoundedAtImInfty.slash

added theorem UpperHalfPlane.IsZeroAtImInfty.slash