Primitives and the modular slash action

This file records how primitives on the upper half-plane transform under the modular slash action: pulling a primitive of F back along the Möbius transformation z ↦ g • z gives a primitive of the weight-2 slash F ∣[2] g. This is what lets a single primitive of F compute the integrals of F(z) dz along all geodesics g • (0, i∞) at once, by comparing its limits at the transformed cusps g • 0 and g • ∞; see TauCeti.NumberTheory.ModularForms.GeodesicIntegral.BetweenCusps.

theorem TauCeti.hasDerivAt_comp_smul {F : UpperHalfPlane → ℂ} {Φ : ℂ → ℂ} (hΦ : ∀ (z : UpperHalfPlane), HasDerivAt Φ (F z) ↑z) {g : GL (Fin 2) ℝ} (hg : 0 < (↑g).det) (τ : UpperHalfPlane) : HasDerivAt (fun (z : ℂ) => Φ ↑(g • ↑UpperHalfPlane.ofComplex z)) (SlashAction.map 2 g F τ) ↑τ

Primitives pull back along Möbius transformations. If Φ is a primitive of F on ℍ, then z ↦ Φ (g • z) is a primitive of the weight-2 slash F ∣[2] g, for g of positive determinant: the weight-2 automorphy factor det g · (cz + d)⁻² is the derivative of z ↦ g • z.