petersson_continuous — Mathlib

English

If f and f' are continuous on the upper half-plane, then the Petersson integrand τ ↦ overline{f(τ)} f'(τ) (Im τ)^k is a continuous function of τ.

Русский

Если f и f' непрерывны на верхней полуплоскости, то интегранд Петершсона по τ непрерывен как функция τ.

LaTeX

$$$\text{Continuous}_{\mathbb{C}}\bigl(\tau \mapsto \overline{f(\tau)} f'(\tau) (\Im \tau)^k\bigr)$$$

Lean4

@[fun_prop]
theorem petersson_continuous (k : ℤ) {f f' : ℍ → ℂ} (hf : Continuous f) (hf' : Continuous f') :
    Continuous (petersson k f f') := by
  unfold petersson
  fun_prop (disch := simp [im_ne_zero _])

Похожие утверждения