Slash Invariance of Serre Derivative of E₂

This file proves that the Serre derivative serre_D 1 E₂ is weight-4 slash-invariant under SL(2,ℤ), despite E₂ itself not being modular.

Main results

• D_D₂ : Derivative of the anomaly function D₂: D(D₂ γ) z = -c²/denom²
• MDifferentiable_D₂ : D₂ γ is MDifferentiable
• serre_DE₂_slash_invariant : serre_D 1 E₂ is weight-4 slash-invariant

Strategy

The key insight is that under the slash action:

• E₂ ∣[2] γ = E₂ - α * D₂ γ where α = 3/π²
• D(D₂ γ) = -c²/denom² where c = γ₁₀
• The anomaly terms cancel because α - α² * π²/3 = 0 when α = 3/π²

Helper lemmas for derivative of anomaly function D₂

theorem D_D₂ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane) : D (D₂ γ) z = -↑(↑γ 1 0) ^ 2 / UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ 2

The D-derivative of the anomaly function D₂. D₂ γ z = 2πi · (γ₁₀ / denom γ z), so D(D₂ γ) = (2πi)⁻¹ · d/dz[2πi · c / denom] = -c² / denom²

MDifferentiable infrastructure for D₂

theorem MDifferentiable_D₂ (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) (D₂ γ)

D₂ γ is MDifferentiable: it's a constant divided by a linear polynomial.

Slash invariance of serre_D 1 E₂

This is the hard part: E₂ is NOT modular, so we cannot use serre_D_slash_invariant. We must prove directly that the non-modular terms cancel.

theorem serre_DE₂_slash_invariant (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ) : SlashAction.map 4 γ (serre_D 1 E₂) = serre_D 1 E₂

The Serre derivative of E₂ is weight-4 slash-invariant. This requires explicit computation since E₂ is not modular.

Proof strategy: Write serre_D 1 E₂ = serre_D 2 E₂ + (1/12) E₂². Then:

• (serre_D 2 E₂) ∣[4] γ = serre_D 2 (E₂ ∣[2] γ) by serre_D_slash_equivariant
• E₂ ∣[2] γ = E₂ - α D₂ γ where α = 1/(2ζ(2)) = 3/π²
• (E₂²) ∣[4] γ = (E₂ ∣[2] γ)²

After expansion, the anomaly terms involving D₂ γ and D(D₂ γ) cancel using:

• D(D₂ γ) = -c²/denom² (from D_D₂)
• The identity α = α² π²/3 (from ζ(2) = π²/6)