noncomputable def ResToImagAxis (F : UpperHalfPlane → ℂ) : ℝ → ℂ

Restrict a function F : ℍ → ℂ to the positive imaginary axis, i.e. t ↦ F (I * t). If $t \le 0$, then F (I * t) is not defined, and we return 0 in that case.

Equations

• ResToImagAxis F t = if ht : 0 < t then F ⟨Complex.I * ↑t, ⋯⟩ else 0

noncomputable def Function.resToImagAxis (F : UpperHalfPlane → ℂ) : ℝ → ℂ

Dot notation alias for ResToImagAxis.

Equations

• Function.resToImagAxis F = ResToImagAxis F

@[simp]

theorem Function.resToImagAxis_eq_resToImagAxis (F : UpperHalfPlane → ℂ) : resToImagAxis F = ResToImagAxis F

@[simp]

theorem Function.resToImagAxis_apply (F : UpperHalfPlane → ℂ) (t : ℝ) : resToImagAxis F t = ResToImagAxis F t

noncomputable def ResToImagAxis.Real (F : UpperHalfPlane → ℂ) : Prop

Function $F : \mathbb{H} \to \mathbb{C}$ whose restriction to the imaginary axis is real-valued, i.e. imaginary part is zero.

Equations

• ResToImagAxis.Real F = ∀ (t : ℝ), 0 < t → (Function.resToImagAxis F t).im = 0

noncomputable def ResToImagAxis.Pos (F : UpperHalfPlane → ℂ) : Prop

Function $F : \mathbb{H} \to \mathbb{C}$ is real and positive on the imaginary axis.

Equations

• ResToImagAxis.Pos F = (ResToImagAxis.Real F ∧ ∀ (t : ℝ), 0 < t → 0 < (Function.resToImagAxis F t).re)

noncomputable def ResToImagAxis.EventuallyPos (F : UpperHalfPlane → ℂ) : Prop

Function $F : \mathbb{H} \to \mathbb{C}$ whose restriction to the imaginary axis is eventually positive, i.e. there exists $t_0 > 0$ such that for all $t \ge t_0$, $F(it)$ is real and positive.

Equations

• ResToImagAxis.EventuallyPos F = (ResToImagAxis.Real F ∧ ∃ (t₀ : ℝ), 0 < t₀ ∧ ∀ (t : ℝ), t₀ ≤ t → 0 < (Function.resToImagAxis F t).re)

theorem ResToImagAxis.Differentiable (F : UpperHalfPlane → ℂ) (hF : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) F) (t : ℝ) (ht : 0 < t) : DifferentiableAt ℝ (Function.resToImagAxis F) t

theorem ResToImagAxis.SlashActionS (F : UpperHalfPlane → ℂ) (k : ℤ) {t : ℝ} (ht : 0 < t) : Function.resToImagAxis (SlashAction.map k ModularGroup.S F) t = Complex.I ^ (-k) * ↑t ^ (-k) * Function.resToImagAxis F (1 / t)

Restriction and slash action under S: $(F |_k S) (it) = (it)^{-k} * F(it)$

theorem ResToImagAxis.Real.add {F G : UpperHalfPlane → ℂ} (hF : Real F) (hG : Real G) : Real (F + G)

Realenss, positivity and essential positivity are closed under the addition and multiplication.

theorem ResToImagAxis.Real.mul {F G : UpperHalfPlane → ℂ} (hF : Real F) (hG : Real G) : Real (F * G)

theorem ResToImagAxis.Real.smul {F : UpperHalfPlane → ℂ} {c : ℝ} (hF : Real F) : Real (c • F)

theorem ResToImagAxis.Pos.add {F G : UpperHalfPlane → ℂ} (hF : Pos F) (hG : Pos G) : Pos (F + G)

theorem ResToImagAxis.Pos.mul {F G : UpperHalfPlane → ℂ} (hF : Pos F) (hG : Pos G) : Pos (F * G)

theorem ResToImagAxis.Pos.smul {F : UpperHalfPlane → ℂ} {c : ℝ} (hF : Pos F) (hc : 0 < c) : Pos fun (z : UpperHalfPlane) => ↑c * F z

theorem ResToImagAxis.EventuallyPos.add {F G : UpperHalfPlane → ℂ} (hF : EventuallyPos F) (hG : EventuallyPos G) : EventuallyPos (F + G)

theorem ResToImagAxis.EventuallyPos.mul {F G : UpperHalfPlane → ℂ} (hF : EventuallyPos F) (hG : EventuallyPos G) : EventuallyPos (F * G)

theorem ResToImagAxis.EventuallyPos.smul {F : UpperHalfPlane → ℂ} {c : ℝ} (hF : EventuallyPos F) (hc : 0 < c) : EventuallyPos fun (z : UpperHalfPlane) => ↑c * F z

Polynomial decay of functions with exponential bounds

This section establishes that if a function F : ℍ → ℂ is O(exp(-c * im τ)) at infinity, then t^s * F(it) → 0 as t → ∞ for any real power s.

One application is to cusp forms, which satisfy such exponential decay bounds.

theorem isBigO_resToImagAxis_of_isBigO_atImInfty {F : UpperHalfPlane → ℂ} {c : ℝ} (_hc : 0 < c) (hF : F =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)) : Function.resToImagAxis F =O[Filter.atTop] fun (t : ℝ) => Real.exp (-c * t)

If F : ℍ → ℂ is O(exp(-c * im τ)) at atImInfty for some c > 0, then the restriction to the imaginary axis t ↦ F(it) is O(exp(-c * t)) at atTop.

theorem tendsto_rpow_mul_of_isBigO_exp {g : ℝ → ℂ} {s b : ℝ} (hb : 0 < b) (hg : g =O[Filter.atTop] fun (t : ℝ) => Real.exp (-b * t)) : Filter.Tendsto (fun (t : ℝ) => ↑t ^ ↑s * g t) Filter.atTop (nhds 0)

The analytic kernel: if g : ℝ → ℂ is eventually bounded by C * exp(-b * t) for some b > 0, then t^s * g(t) → 0 as t → ∞ for any real power s.

This follows from the fact that t^s * exp(-b * t) → 0 (mathlib's tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero) combined with the big-O transfer lemma.

theorem tendsto_rpow_mul_resToImagAxis_of_isBigO_exp {F : UpperHalfPlane → ℂ} {c : ℝ} (hc : 0 < c) (hF : F =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-c * τ.im)) (s : ℝ) : Filter.Tendsto (fun (t : ℝ) => ↑t ^ ↑s * Function.resToImagAxis F t) Filter.atTop (nhds 0)

If F : ℍ → ℂ is O(exp(-c * im τ)) at atImInfty for some c > 0, then t^s * F(it) → 0 as t → ∞ for any real power s.

theorem cuspForm_rpow_mul_resToImagAxis_tendsto_zero {n : ℕ} {k : ℤ} {F : Type u_1} [NeZero n] [FunLike F UpperHalfPlane ℂ] [CuspFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma n)) k] (f : F) (s : ℝ) : Filter.Tendsto (fun (t : ℝ) => ↑t ^ ↑s * Function.resToImagAxis (⇑f) t) Filter.atTop (nhds 0)

For a cusp form f of level Γ(n), we have t^s * f(it) → 0 as t → ∞ for any real power s.

This follows from the exponential decay of cusp forms at infinity: f = O(exp(-2π τ.im / n)).

Fourier expansion approach for polynomial decay

This section provides an alternative approach to polynomial decay that works directly from Fourier expansions. If F has a Fourier expansion ∑_{m≥0} a_m exp(2πi(m+n₀)z) with n₀ > 0, then F = O(exp(-2π n₀ · im z)) at atImInfty, which gives t^s * F(it) → 0.

This is useful for functions with q-expansions starting at a positive index (like (E₂E₄ - E₆)²).

theorem isBigO_atImInfty_of_fourier_shift {F : UpperHalfPlane → ℂ} {a : ℕ → ℂ} {n₀ : ℕ} {c : ℝ} (_hn₀ : 0 < n₀) (_hc : 0 < c) (hF : ∀ (z : UpperHalfPlane), F z = ∑' (m : ℕ), a m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(m + n₀) * ↑z)) (ha : Summable fun (m : ℕ) => ‖a m‖ * Real.exp (-(2 * Real.pi * c) * ↑m)) : F =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (-(2 * Real.pi * ↑n₀) * z.im)

If F has a Fourier expansion ∑_{m≥0} a_m exp(2πi(m+n₀)z) with n₀ > 0, and the coefficients are absolutely summable at height im z = c, then F = O(exp(-2π n₀ · im z)) at atImInfty.

The key bound is: for im z ≥ c, ‖F(z)‖ ≤ (∑_m ‖a_m‖ · exp(-2π c m)) · exp(-2π n₀ · im z)

theorem tendsto_rpow_mul_resToImagAxis_of_fourier_shift {F : UpperHalfPlane → ℂ} {a : ℕ → ℂ} {n₀ : ℕ} {c : ℝ} (hn₀ : 0 < n₀) (hc : 0 < c) (hF : ∀ (z : UpperHalfPlane), F z = ∑' (m : ℕ), a m * Complex.exp (2 * ↑Real.pi * Complex.I * ↑(m + n₀) * ↑z)) (ha : Summable fun (m : ℕ) => ‖a m‖ * Real.exp (-(2 * Real.pi * c) * ↑m)) (s : ℝ) : Filter.Tendsto (fun (t : ℝ) => ↑t ^ ↑s * Function.resToImagAxis F t) Filter.atTop (nhds 0)

If F has a Fourier expansion starting at index n₀ > 0 with absolutely summable coefficients at height c > 0, then t^s * F(it) → 0 as t → ∞ for any real power s.

This converts a Fourier expansion representation directly into polynomial decay on the imaginary axis.