Theorems · Theorem · number theory

UpperHalfPlane.isBoundedAtImInfty_of_hasSum_qExpansion

∀ {h : ℝ} {f : UpperHalfPlane → ℂ} {c : ℕ → ℂ},
  0 < h →
    (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
      UpperHalfPlane.IsBoundedAtImInfty f

A function on the upper half plane that is given everywhere by a convergent q-expansion with non-negative exponents, f τ = ∑' m, c m * 𝕢 h τ ^ m, is bounded at i∞. This is a converse to hasSum_qExpansion: there, boundedness is a hypothesis used to produce the q-expansion, while here convergence of the q-expansion is enough to deduce boundedness.

Defined in

Mathlib.NumberTheory.ModularForms.QExpansion

Cited by

1 results in Mathlib

Foundations

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