Research proof index

Δ transforms under S as: Δ(-1/z) = z¹² · Δ(z) -/ lemma Δ_S_transform (z : ℍ) : Δ (ModularGroup.S • z) = z ^ (12 : ℕ) * Δ z := by have h := Discriminant_S_invariant simp only [funext_iff] at h specialize h z rw [SL_slash_apply] at h simp only [ModularGroup.denom_S, zpow_neg] at h field_simp [ne_zero z] at h rw [h, mul_comm] theorem Delta_boundedfactor : Te...

Derivative of denom^(-k): d/dz[(cz+d)^(-k)] = -k * c * (cz+d)^(-k-1).

The derivative of FmodGReal is (-2π) * L₁,₀(it) / G(it)².

Derivative of the Möbius transformation: d/dz[(az+b)/(cz+d)] = 1/(cz+d)². Uses det(γ) = 1: a(cz+d) - c(az+b) = ad - bc = 1.

Chain rule for restriction to imaginary axis: d/dt F(it) = -2π * (D F)(it). This connects the real derivative along the imaginary axis to the normalized derivative D. The key computation is: - The imaginary axis is parametrized by g(t) = I * t - By chain rule: d/dt F(it) = (dF/dz)(it) · (d/dt)(it) = F'(it) · I - Since D = (2πi)⁻¹ · d/dz, we have F' = 2π...

Differentiability of t ↦ jacobiTheta₂(t/2, t) at points in the upper half-plane.