English
Under a Moebius action by SL(2,ℤ), eisSummand transforms by a simple weight-k factor times the transformed index.
Русский
При действии Мёбиуса элементами SL(2,ℤ) функция eisSummand преобразуется умножением на фактор веса k и перестановкой индекса.
LaTeX
$$$\mathrm{eisSummand}(k,i,A\cdot z) = \big(\mathrm{denom}(A,z)\big)^k \cdot \mathrm{eisSummand}\big(k,i\,\cdot\! A,z\big).$$$
Lean4
/-- How the `eisSummand` function changes under the Moebius action. -/
theorem eisSummand_SL2_apply (k : ℤ) (i : (Fin 2 → ℤ)) (A : SL(2, ℤ)) (z : ℍ) :
eisSummand k i (A • z) = (denom A z) ^ k * eisSummand k (i ᵥ* A) z :=
by
simp only [eisSummand, vecMul, vec2_dotProduct, denom, UpperHalfPlane.specialLinearGroup_apply]
have h (a b c d u v : ℂ) (hc : c * z + d ≠ 0) :
(u * ((a * z + b) / (c * z + d)) + v) ^ (-k) = (c * z + d) ^ k * ((u * a + v * c) * z + (u * b + v * d)) ^ (-k) :=
by
replace hc : z * c + d ≠ 0 := by convert hc using 1; ring
field_simp
simp [div_zpow]
ring_nf
simpa using h (hc := denom_ne_zero A z) ..
