Periodic holomorphic functions

We show that if f : ℂ → ℂ satisfies f (z + h) = f z, for some nonzero real h, then there is a function F such that f z = F (exp (2 * π * I * z / h)) for all z; and if f is holomorphic at some z, then F is holomorphic at exp (2 * π * I * z / h).

We also show (using Riemann's removable singularity theorem) that if f is holomorphic and bounded for all sufficiently large im z, then F extends to a holomorphic function on a neighbourhood of 0. As a consequence, if f tends to zero as im z → ∞, then in fact it decays exponentially to zero. These results are important in the theory of modular forms.

def Function.Periodic.qParam (h : ℝ) (z : ℂ) : ℂ

Parameter for q-expansions, qParam h z = exp (2 * π * I * z / h)

Equations

• Function.Periodic.qParam h z = Complex.exp (2 * ↑Real.pi * Complex.I * z / ↑h)

def Function.Periodic.invQParam (h : ℝ) (q : ℂ) : ℂ

One-sided inverse of qParam h.

Equations

• Function.Periodic.invQParam h q = ↑h / (2 * ↑Real.pi * Complex.I) * Complex.log q

theorem Function.Periodic.norm_qParam (h : ℝ) (z : ℂ) : ‖qParam h z‖ = Real.exp (-2 * Real.pi * z.im / h)

@[deprecated Function.Periodic.norm_qParam (since := "2025-02-17")]

theorem Function.Periodic.abs_qParam (h : ℝ) (z : ℂ) : ‖qParam h z‖ = Real.exp (-2 * Real.pi * z.im / h)

Alias of Function.Periodic.norm_qParam.

theorem Function.Periodic.im_invQParam (h : ℝ) (q : ℂ) : (invQParam h q).im = -h / (2 * Real.pi) * Real.log ‖q‖

theorem Function.Periodic.qParam_right_inv {h : ℝ} (hh : h ≠ 0) {q : ℂ} (hq : q ≠ 0) : qParam h (invQParam h q) = q

theorem Function.Periodic.qParam_left_inv_mod_period {h : ℝ} (hh : h ≠ 0) (z : ℂ) : ∃ (m : ℤ), invQParam h (qParam h z) = z + ↑m * ↑h

theorem Function.Periodic.norm_qParam_lt_iff {h : ℝ} (hh : 0 < h) (A : ℝ) (z : ℂ) : ‖qParam h z‖ < Real.exp (-2 * Real.pi * A / h) ↔ A < z.im

@[deprecated Function.Periodic.norm_qParam_lt_iff (since := "2025-02-17")]

theorem Function.Periodic.abs_qParam_lt_iff {h : ℝ} (hh : 0 < h) (A : ℝ) (z : ℂ) : ‖qParam h z‖ < Real.exp (-2 * Real.pi * A / h) ↔ A < z.im

Alias of Function.Periodic.norm_qParam_lt_iff.

theorem Function.Periodic.qParam_tendsto {h : ℝ} (hh : 0 < h) : Filter.Tendsto (qParam h) (Filter.comap Complex.im Filter.atTop) (nhdsWithin 0 {0}ᶜ)

theorem Function.Periodic.invQParam_tendsto {h : ℝ} (hh : 0 < h) : Filter.Tendsto (invQParam h) (nhdsWithin 0 {0}ᶜ) (Filter.comap Complex.im Filter.atTop)

def Function.Periodic.cuspFunction (h : ℝ) (f : ℂ → ℂ) : ℂ → ℂ

The function q ↦ f (invQParam h q), extended by a non-canonical choice of limit at 0.

Equations

• Function.Periodic.cuspFunction h f = Function.update (f ∘ Function.Periodic.invQParam h) 0 (limUnder (nhdsWithin 0 {0}ᶜ) (f ∘ Function.Periodic.invQParam h))

theorem Function.Periodic.cuspFunction_eq_of_nonzero (h : ℝ) (f : ℂ → ℂ) {q : ℂ} (hq : q ≠ 0) : cuspFunction h f q = f (invQParam h q)

theorem Function.Periodic.cuspFunction_zero_eq_limUnder_nhds_ne (h : ℝ) (f : ℂ → ℂ) : cuspFunction h f 0 = limUnder (nhdsWithin 0 {0}ᶜ) (cuspFunction h f)

theorem Function.Periodic.eq_cuspFunction {h : ℝ} {f : ℂ → ℂ} (hh : h ≠ 0) (hf : Periodic f ↑h) (z : ℂ) : cuspFunction h f (qParam h z) = f z

theorem Function.Periodic.differentiableAt_cuspFunction {h : ℝ} {f : ℂ → ℂ} (hh : h ≠ 0) (hf : Periodic f ↑h) {z : ℂ} (hol_z : DifferentiableAt ℂ f z) : DifferentiableAt ℂ (cuspFunction h f) (qParam h z)

Key technical lemma: the function cuspFunction h f is differentiable at the images of differentiability points of f (even if invQParam is not differentiable there).

theorem Function.Periodic.eventually_differentiableAt_cuspFunction_nhds_ne_zero {h : ℝ} {f : ℂ → ℂ} (hh : 0 < h) (hf : Periodic f ↑h) (h_hol : ∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) : ∀ᶠ (q : ℂ) in nhdsWithin 0 {0}ᶜ, DifferentiableAt ℂ (cuspFunction h f) q

theorem Function.Periodic.boundedAtFilter_cuspFunction {h : ℝ} {f : ℂ → ℂ} (hh : 0 < h) (h_bd : (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f) : (nhdsWithin 0 {0}ᶜ).BoundedAtFilter (cuspFunction h f)

theorem Function.Periodic.cuspFunction_zero_of_zero_at_inf {h : ℝ} {f : ℂ → ℂ} (hh : 0 < h) (h_zer : (Filter.comap Complex.im Filter.atTop).ZeroAtFilter f) : cuspFunction h f 0 = 0

theorem Function.Periodic.differentiableAt_cuspFunction_zero {h : ℝ} {f : ℂ → ℂ} (hh : 0 < h) (hf : Periodic f ↑h) (h_hol : ∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) (h_bd : (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f) : DifferentiableAt ℂ (cuspFunction h f) 0

theorem Function.Periodic.tendsto_at_I_inf {h : ℝ} {f : ℂ → ℂ} (hh : 0 < h) (hf : Periodic f ↑h) (h_hol : ∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) (h_bd : (Filter.comap Complex.im Filter.atTop).BoundedAtFilter f) : Filter.Tendsto f (Filter.comap Complex.im Filter.atTop) (nhds (cuspFunction h f 0))

If f is periodic, and holomorphic and bounded near I∞, then it tends to a limit at I∞, and this limit is the value of its cusp function at 0.

theorem Function.Periodic.exp_decay_of_zero_at_inf {h : ℝ} {f : ℂ → ℂ} (hh : 0 < h) (hf : Periodic f ↑h) (h_hol : ∀ᶠ (z : ℂ) in Filter.comap Complex.im Filter.atTop, DifferentiableAt ℂ f z) (h_zer : (Filter.comap Complex.im Filter.atTop).ZeroAtFilter f) : f =O[Filter.comap Complex.im Filter.atTop] fun (z : ℂ) => Real.exp (-2 * Real.pi * z.im / h)

If f is periodic, holomorphic near I∞, and tends to zero at I∞, then in fact it tends to zero exponentially fast.