English
For k ∈ ℤ, f, f' : ℍ → ℂ, g ∈ GL(2, ℝ) and τ ∈ ℍ, the Petersson integrand transforms by petersson_k(f|[k]g, f'|[k]g)(τ) = |det g|^{k-2} σ_g(petersson_k(f,f')(g·τ)).
Русский
Для целого k, двух функций f, f' и элемента g ∈ GL(2, ℝ) интегранд Петершсона трансформируется по формуле: petersson_k(f|_k g, f'|_k g)(τ) = |det g|^{k-2} σ_g(petersson_k(f,f')(g·τ)).
LaTeX
$$$\mathrm{petersson}_k(f|[k]g, f'|[k]g)(\tau) = |\det g|^{k-2} \, σ(g)\bigl( \mathrm{petersson}_k(f,f')(g\cdot \tau) \bigr)$$$
Lean4
theorem petersson_slash (k : ℤ) (f f' : ℍ → ℂ) (g : GL (Fin 2) ℝ) (τ : ℍ) :
petersson k (f ∣[k] g) (f' ∣[k] g) τ = |g.det.val| ^ (k - 2) * σ g (petersson k f f' (g • τ)) :=
by
set D := |g.det.val|
have hD : (D : ℂ) ≠ 0 := mod_cast abs_ne_zero.mpr g.det_ne_zero
set j := denom g τ
calc
petersson k (f ∣[k] g) (f' ∣[k] g) τ
_ = D ^ (k - 2 + k) * conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (τ.im ^ k * j.normSq ^ (-k)) :=
by
simp [Complex.normSq_eq_conj_mul_self, (by abel : k - 2 + k = (k - 1) + (k - 1)), petersson, zpow_add₀ hD,
mul_zpow, ModularForm.slash_def, -Matrix.GeneralLinearGroup.val_det_apply]
ring
_ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (D * τ.im / j.normSq) ^ k) :=
by
rw [div_zpow, mul_zpow, zpow_neg, div_eq_mul_inv, zpow_add₀ hD]
ring
_ = D ^ (k - 2) * (conj (σ g (f (g • τ))) * σ g (f' (g • τ)) * (im (g • τ)) ^ k) := by
rw [im_smul_eq_div_normSq, Complex.ofReal_div, Complex.ofReal_mul]
_ = D ^ (k - 2) * σ g (petersson k f f' (g • τ)) := by simp [petersson, σ_conj]
