The S-transformation of the complex extension of a slash-invariant form

For a weight-k slash-invariant form f whose group contains S = !![0, -1; 1, 0], the transformation law f (S • τ) = τ ^ k * f τ transports through ofComplex to the identity (⇑f ∘ ofComplex) (-1 / w) = w ^ k * (⇑f ∘ ofComplex) w on the open upper half-plane. Differentiability of the extension transports across the S-orbit through the same identity, and differentiating it expresses the logarithmic derivative at w through the logarithmic derivative at -1 / w up to the weight term k / w — the integrand identity behind the arc self-pairing of the valence-formula contour integral.

Main declarations

• TauCeti.ModularForm.comp_ofComplex_S_transform: the S-transformation law of ⇑f ∘ ofComplex.
• TauCeti.ModularForm.differentiableAt_comp_ofComplex_S_transform: differentiability transports across the S-orbit.
• TauCeti.ModularForm.logDeriv_comp_ofComplex_S_transform: the S-transformation law of the logarithmic derivative.

theorem TauCeti.ModularForm.comp_ofComplex_S_transform {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {w : ℂ} (hw : 0 < w.im) : (⇑f ∘ ↑UpperHalfPlane.ofComplex) (-1 / w) = w ^ k * (⇑f ∘ ↑UpperHalfPlane.ofComplex) w

The S-transformation law of the complex extension of a slash-invariant form, at the points of the open upper half-plane.

theorem TauCeti.ModularForm.differentiableAt_comp_ofComplex_S_transform {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {w : ℂ} (hw : 0 < w.im) (hd : DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) w) : DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (-1 / w)

Differentiability of the complex extension of a slash-invariant form transports across the S-orbit.

theorem TauCeti.ModularForm.logDeriv_comp_ofComplex_S_transform {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hS : ModularGroup.S ∈ Γ) {w : ℂ} (hw : 0 < w.im) (hd : DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) w) (hfw : (⇑f ∘ ↑UpperHalfPlane.ofComplex) w ≠ 0) : logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) w = logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (-1 / w) / w ^ 2 - ↑k / w

The S-transformation law of the logarithmic derivative of the complex extension of a slash-invariant form, at points of the open upper half-plane where the extension is differentiable and does not vanish.