Theorems · Theorem · number theory

ModularGroup.exists_bound_of_invariant_of_isBigO

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

A function on ℍ which is invariant under SL(2, ℤ), and is O ((im τ) ^ t) at I∞ for some 0 ≤ t, is bounded on ℍ by a constant multiple of (max (im τ) (1 / im τ)) ^ t. This will be applied to f τ * (im τ) ^ (k / 2) for f a modular form of weight k, taking t = 0 if f is cuspidal, and t = k / 2 otherwise.

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

2 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroup