Theorems · Theorem · number theory

ModularGroup.exists_bound_of_subgroup_invariant

∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsBoundedAtImInfty fun τ => f (g • τ)) →
      ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic],
        (∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) → ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C

A function on ℍ which is invariant under an arithmetic subgroup and bounded at all cusps, is uniformly bounded.

Defined in

Mathlib.NumberTheory.ModularForms.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

SeminormedAddCommGroupSubgroup.IsArithmetic