QExpansion

Limits at infinity

In this file we establishes basic results about q-expansions. The results are put under the QExp namespace.

TODO:

• Are any of these results in Mathlib, perhaps phrased in some other way?

theorem QExp.tendsto_nat (a : ℕ → ℂ) (ha : Summable fun (n : ℕ) => ‖a n‖ * Real.exp (-2 * Real.pi * ↑n)) : Filter.Tendsto (fun (z : UpperHalfPlane) => ∑' (n : ℕ), a n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑n)) UpperHalfPlane.atImInfty (nhds (a 0))

theorem QExp.tendsto_int (a : ℤ → ℂ) (ha : Summable fun (n : ℤ) => ‖a n‖ * Real.exp (-2 * Real.pi * ↑n)) (ha' : ∀ n < 0, a n = 0) : Filter.Tendsto (fun (z : UpperHalfPlane) => ∑' (n : ℤ), a n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z * ↑n)) UpperHalfPlane.atImInfty (nhds (a 0))