English
Jacobi’s theta function is compatible with S-action on the upper half-plane: θ(S · τ) = (-I τ)^{1/2} θ(τ), up to conventional interpretation of the action.
Русский
Функция θ совместима с действием S на верхнюю полуплоскость: θ(S · τ) = (-i τ)^{1/2} θ(τ).
LaTeX
$$$\operatorname{jacobiTheta}(S \cdot \tau) = (-\mathrm{i} \tau)^{1/2} \operatorname{jacobiTheta}(\tau).$$$
Lean4
theorem jacobiTheta_S_smul (τ : ℍ) : jacobiTheta ↑(ModularGroup.S • τ) = (-I * τ) ^ (1 / 2 : ℂ) * jacobiTheta τ :=
by
have h0 : (τ : ℂ) ≠ 0 := ne_of_apply_ne im (zero_im.symm ▸ ne_of_gt τ.2)
have h1 : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
rw [Ne, cpow_eq_zero_iff, not_and_or]
exact Or.inl <| mul_ne_zero (neg_ne_zero.mpr I_ne_zero) h0
simp_rw [UpperHalfPlane.modular_S_smul, jacobiTheta_eq_jacobiTheta₂, ← ofReal_zero]
norm_cast
simp_rw [jacobiTheta₂_functional_equation 0 τ, zero_pow two_ne_zero, mul_zero, zero_div, Complex.exp_zero, mul_one, ←
mul_assoc, mul_one_div, div_self h1, one_mul, UpperHalfPlane.coe_mk, inv_neg, neg_div, one_div]
