Commit 2024-11-20 14:09 edcdc3e1

View on Github →

feat(UpperHalfPlane): weaken assumptions of multiple atImInfty lemmas (#16015) In this PR, I weaken some assumptions so that they can be applied more widely (more specifically, to my use case :) ) I also renamed some lemmas because they sounded weird.

Estimated changes

Modified Mathlib/Analysis/Asymptotics/Asymptotics.lean

modified theorem Asymptotics.isLittleO_one_iff

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

added theorem UpperHalfPlane.IsZeroAtImInfty.isBoundedAtImInfty

deleted theorem UpperHalfPlane.bounded_mem

added theorem UpperHalfPlane.isBoundedAtImInfty_iff

added theorem UpperHalfPlane.isZeroAtImInfty_iff

deleted theorem UpperHalfPlane.zero_at_im_infty

Modified Mathlib/NumberTheory/ModularForms/Basic.lean

Modified Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

Modified Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean

modified theorem Filter.ZeroAtFilter.boundedAtFilter