jacobiTheta₂_conj — Mathlib

English

Complex conjugation intertwines Jacobi theta: conj(θ₂(z,τ)) = θ₂(conj z, −conj τ).

Русский

Комплекс–сопряжение сохраняет θ₂: conj(θ₂(z,τ)) = θ₂(conj z, −conj τ).

LaTeX

$$$\overline{\theta_2(z,\tau)} = \theta_2(\overline{z}, -\overline{\tau})$$$

Lean4

theorem jacobiTheta₂_conj (z τ : ℂ) : conj (jacobiTheta₂ z τ) = jacobiTheta₂ (conj z) (-conj τ) :=
  by
  rw [← jacobiTheta₂_neg_left, jacobiTheta₂, conj_tsum]
  congr 2 with n
  simp only [jacobiTheta₂_term, mul_neg, ← exp_conj, map_add, map_neg, map_mul, map_ofNat, conj_ofReal, conj_I,
    map_intCast, neg_mul, neg_neg, map_pow]

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