Theorems · Theorem · number theory

Derivative.normalizedDerivOfComplex_SL_slash

∀ {k : ℤ} {F : UpperHalfPlane → ℂ},
  MDiff F →
    ∀ {γ : Matrix.SpecialLinearGroup (Fin 2) ℤ},
      Derivative.normalizedDerivOfComplex (SlashAction.map k γ F) =
        SlashAction.map (k + 2) γ (Derivative.normalizedDerivOfComplex F) - fun z =>
          ↑k * (2 * ↑Real.pi * Complex.I)⁻¹ *
              (↑(↑γ 1 0) /
                UpperHalfPlane.denom
                  (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z) *
            SlashAction.map k γ F z

The SL(2, ℤ) case of normalizedDerivOfComplex_slash, where the determinant factor is 1.

Defined in

Mathlib.NumberTheory.ModularForms.Derivative

Cited by

1 results in Mathlib

Foundations

Depth 213 from the axioms · uses propext, Classical.choice, Quot.sound