jacobiTheta₂'_conj — Mathlib

English

The map zτ ↦ θ₂'(z,τ) commutes with the star-structure, i.e., θ₂' maps under conjugation to θ₂' of conjugated arguments.

Русский

Картирование по сопряжению применимо к θ₂': θ₂'(z,τ) под конюгацией становится θ₂'(conj z, -conj τ).

LaTeX

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

Lean4

theorem jacobiTheta₂'_conj (z τ : ℂ) : conj (jacobiTheta₂' z τ) = jacobiTheta₂' (conj z) (-conj τ) :=
  by
  rw [← neg_inj, ← jacobiTheta₂'_neg_left, jacobiTheta₂', jacobiTheta₂', conj_tsum, ← tsum_neg]
  congr 1 with n
  simp_rw [jacobiTheta₂'_term, jacobiTheta₂_term, map_mul, ← Complex.exp_conj, map_add, map_mul, ← ofReal_intCast, ←
    ofReal_ofNat, map_pow, conj_ofReal, conj_I]
  ring_nf

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