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.

Author: grhkm21

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -1149,7 +1149,7 @@ theorem isLittleO_const_iff_isLittleO_one {c : F''} (hc : c ≠ 0) :
    fun h => h.trans_isBigO <| isBigO_const_const _ hc _⟩
 
 @[simp]
-theorem isLittleO_one_iff : f' =o[l] (fun _x => 1 : α → F) ↔ Tendsto f' l (𝓝 0) := by
+theorem isLittleO_one_iff {f : α → E'''} : f =o[l] (fun _x => 1 : α → F) ↔ Tendsto f l (𝓝 0) := by
   simp only [isLittleO_iff, norm_one, mul_one, Metric.nhds_basis_closedBall.tendsto_right_iff,
     Metric.mem_closedBall, dist_zero_right]
 

Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

@@ -53,19 +53,22 @@ def zeroAtImInftySubmodule (α : Type*) [NormedField α] : Submodule α (ℍ →
 def boundedAtImInftySubalgebra (α : Type*) [NormedField α] : Subalgebra α (ℍ → α) :=
   boundedFilterSubalgebra _ atImInfty
 
-nonrec theorem IsBoundedAtImInfty.mul {f g : ℍ → ℂ} (hf : IsBoundedAtImInfty f)
-    (hg : IsBoundedAtImInfty g) : IsBoundedAtImInfty (f * g) := by
-  simpa only [Pi.one_apply, mul_one, norm_eq_abs] using hf.mul hg
-
-theorem bounded_mem (f : ℍ → ℂ) :
-    IsBoundedAtImInfty f ↔ ∃ M A : ℝ, ∀ z : ℍ, A ≤ im z → abs (f z) ≤ M := by
+theorem isBoundedAtImInfty_iff {α : Type*} [Norm α] {f : ℍ → α} :
+    IsBoundedAtImInfty f ↔ ∃ M A : ℝ, ∀ z : ℍ, A ≤ im z → ‖f z‖ ≤ M := by
   simp [IsBoundedAtImInfty, BoundedAtFilter, Asymptotics.isBigO_iff, Filter.Eventually,
     atImInfty_mem]
 
-theorem zero_at_im_infty (f : ℍ → ℂ) :
-    IsZeroAtImInfty f ↔ ∀ ε : ℝ, 0 < ε → ∃ A : ℝ, ∀ z : ℍ, A ≤ im z → abs (f z) ≤ ε :=
-  (atImInfty_basis.tendsto_iff Metric.nhds_basis_closedBall).trans <| by
-    simp only [true_and, mem_closedBall_zero_iff]; rfl
+@[deprecated (since := "2024-08-27")] alias _root_.bounded_mem := isBoundedAtImInfty_iff
+
+theorem isZeroAtImInfty_iff {α : Type*} [SeminormedAddGroup α] {f : ℍ → α} :
+    IsZeroAtImInfty f ↔ ∀ ε : ℝ, 0 < ε → ∃ A : ℝ, ∀ z : ℍ, A ≤ im z → ‖f z‖ ≤ ε :=
+  (atImInfty_basis.tendsto_iff Metric.nhds_basis_closedBall).trans <| by simp
+
+@[deprecated (since := "2024-08-27")] alias _root_.zero_at_im_infty := isZeroAtImInfty_iff
+
+theorem IsZeroAtImInfty.isBoundedAtImInfty {α : Type*} [SeminormedAddGroup α] {f : ℍ → α}
+    (hf : IsZeroAtImInfty f) : IsBoundedAtImInfty f :=
+  hf.boundedAtFilter
 
 lemma tendsto_comap_im_ofComplex :
     Tendsto ofComplex (comap Complex.im atTop) atImInfty := by

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -227,10 +227,7 @@ def mul {k_1 k_2 : ℤ} {Γ : Subgroup SL(2, ℤ)} (f : ModularForm Γ k_1) (g :
   toSlashInvariantForm := f.1.mul g.1
   holo' := f.holo'.mul g.holo'
   bdd_at_infty' A := by
-    -- Porting note: was `by simpa using ...`
-    -- `mul_slash_SL2` is no longer a `simp` and `simpa only [mul_slash_SL2] using ...` failed
-    rw [SlashInvariantForm.coe_mul, mul_slash_SL2]
-    exact (f.bdd_at_infty' A).mul (g.bdd_at_infty' A)
+    simpa only [coe_mul, mul_slash_SL2] using (f.bdd_at_infty' A).mul (g.bdd_at_infty' A)
 
 @[simp]
 theorem mul_coe {k_1 k_2 : ℤ} {Γ : Subgroup SL(2, ℤ)} (f : ModularForm Γ k_1)

Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean

@@ -52,7 +52,7 @@ lemma abs_le_tsum_abs (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ) (hk : 3 ≤ k)
 /-- Eisenstein series are bounded at infinity. -/
 theorem isBoundedAtImInfty_eisensteinSeries_SIF {N : ℕ+} (a : Fin 2 → ZMod N) {k : ℤ} (hk : 3 ≤ k)
     (A : SL(2, ℤ)) : IsBoundedAtImInfty ((eisensteinSeries_SIF a k).toFun ∣[k] A) := by
-  simp_rw [UpperHalfPlane.bounded_mem, eisensteinSeries_SIF] at *
+  simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeries_SIF] at *
   refine ⟨∑'(x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩
   intro z hz
   obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z N.2)

Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean

@@ -71,15 +71,16 @@ if `f =O[l] 1`. -/
 def BoundedAtFilter [Norm β] (l : Filter α) (f : α → β) : Prop :=
   Asymptotics.IsBigO l f (1 : α → ℝ)
 
-theorem ZeroAtFilter.boundedAtFilter [NormedAddCommGroup β] {l : Filter α} {f : α → β}
-    (hf : ZeroAtFilter l f) : BoundedAtFilter l f := by
-  rw [ZeroAtFilter, ← Asymptotics.isLittleO_const_iff (one_ne_zero' ℝ)] at hf
-  exact hf.isBigO
+theorem ZeroAtFilter.boundedAtFilter [SeminormedAddGroup β] {l : Filter α} {f : α → β}
+    (hf : ZeroAtFilter l f) : BoundedAtFilter l f :=
+  ((Asymptotics.isLittleO_one_iff _).mpr hf).isBigO
 
 theorem const_boundedAtFilter [Norm β] (l : Filter α) (c : β) :
     BoundedAtFilter l (Function.const α c : α → β) :=
   Asymptotics.isBigO_const_const c one_ne_zero l
 
+-- TODO(https://github.com/leanprover-community/mathlib4/issues/19288): Remove all Comm in the next
+-- three lemmas. This would require modifying the corresponding general asymptotics lemma.
 nonrec theorem BoundedAtFilter.add [SeminormedAddCommGroup β] {l : Filter α} {f g : α → β}
     (hf : BoundedAtFilter l f) (hg : BoundedAtFilter l g) : BoundedAtFilter l (f + g) := by
   simpa using hf.add hg