petersson_slash_SL — Mathlib

English

For SL(2,ℤ) matrices g, the Petersson transform satisfies petersson_k(f|_k g, f'|_k g)(τ) = petersson_k(f,f')(g·τ).

Русский

Для матриц g из SL(2,ℤ) выполняется: petersson_k(f|_k g, f'|_k g)(τ) = petersson_k(f,f')(g·τ).

LaTeX

$$$\mathrm{petersson}_k\bigl( f|[k]g, f'|[k]g \bigr)(\tau) = \mathrm{petersson}_k(f,f')(g\cdot \tau)$$$

Lean4

theorem petersson_slash_SL (k : ℤ) (f f' : ℍ → ℂ) (g : SL(2, ℤ)) (τ : ℍ) :
    petersson k (f ∣[k] g) (f' ∣[k] g) τ = petersson k f f' (g • τ) := by
  -- need to disable two simp lemmas as they work against `Matrix.SpecialLinearGroup.det_coe`
  simp [σ, ModularForm.SL_slash, petersson_slash, -Matrix.SpecialLinearGroup.map_apply_coe,
    -Matrix.SpecialLinearGroup.coe_matrix_coe]

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