Theorems · Theorem · number theory

ModularGroup.exists_bound_of_subgroup_invariant_of_isArithmetic_of_isBigO

∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    ∀ {t : ℝ},
      0 ≤ t →
        (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
            (fun τ => f (g • τ)) =O[UpperHalfPlane.atImInfty] fun z => z.im ^ t) →
          ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic],
            (∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) →
              ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t

A function on ℍ which is invariant under an arithmetic subgroup of GL(2, ℝ), and satisfies an O((im τ) ^ t) bound at all cusps for some 0 ≤ t, is in fact uniformly bounded by a multiple of (max (im τ) (1 / im τ)) ^ t.

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

2 results in Mathlib

Foundations

Depth 211 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupSubgroup.IsArithmetic