petersson — Mathlib

English

The Petersson integrand for two modular forms f and f' of weight k is given by conj(f(τ)) f'(τ) (Im τ)^k.

Русский

Интегранд Петершсона для двух форм f, f' весa k есть конъюгированное значение f(τ) умноженное на f'(τ) и на Im(τ)^k.

LaTeX

$$$\mathrm{petersson}_k(f,f')(\tau) = \overline{f(\tau)} \cdot f'(\tau) \cdot (\Im \tau)^k$$$

Lean4

/-- The integrand in the Petersson scalar product of two modular forms. -/
noncomputable def petersson (k : ℤ) (f f' : ℍ → ℂ) (τ : ℍ) :=
  conj (f τ) * f' τ * τ.im ^ k

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