jacobiTheta_T_sq_smul — Mathlib

English

Under the S-action, Jacobi’s theta function transforms by a nonzero factor: θ(S^2 · τ) = (-I τ)^{1/2} θ(τ).

Русский

При действии S функция θ трансформируется множителем, не равным нулю: θ(S^2 · τ) = (-i τ)^{1/2} θ(τ).

LaTeX

$$$\operatorname{jacobiTheta}(S^{2} · \tau) = (-\mathrm{i} \tau)^{1/2} \operatorname{jacobiTheta}(\tau).$$$

Lean4

theorem jacobiTheta_T_sq_smul (τ : ℍ) : jacobiTheta (ModularGroup.T ^ 2 • τ :) = jacobiTheta τ :=
  by
  suffices (ModularGroup.T ^ 2 • τ :) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]
  have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := rfl
  simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]
  norm_cast

Похожие утверждения