-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
theorem jacobiTheta₂_functional_equation (z τ : ℂ) : jacobiTheta₂ z τ =
    1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (-π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Proof state:
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
⊢ 0 < (-I * τ).re

Tactic:
simpa only [neg_mul, neg_re, mul_re, I_re, zero_mul, I_im, one_mul, zero_sub, neg_neg] using hτ

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
⊢ τ ≠ 0

Tactic:
contrapose! hτ

Result:
z τ : ℂ
hτ : τ = 0
⊢ τ.im ≤ 0

Proof state:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

Tactic:
rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]

Result:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ

Proof state:
z τ : ℂ
hτ : τ = 0
⊢ τ.im ≤ 0

Tactic:
rw [hτ, zero_im]

Result:
no goals

Proof state:
case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
unfold jacobiTheta₂ jacobiTheta₂_term

Result:
case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Proof state:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ -↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2 =
    ↑π * I * (-1 / τ) * z ^ 2 + (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
field_simp [I_ne_zero]

Result:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑π * (↑n + I * (I * z)) ^ 2 * (τ * τ) =
    (-(↑π * I * z ^ 2 * τ) + (2 * ↑π * I * ↑n * z + -(↑π * I * ↑n ^ 2)) * τ) * (I * τ)

Proof state:
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) * cexp (↑π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]

Result:
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) *
      ∑' (x : ℤ), cexp (↑π * I * (-1 / τ) * z ^ 2 + (2 * ↑π * I * ↑x * (z / τ) + ↑π * I * ↑x ^ 2 * (-1 / τ)))

Proof state:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
have : (-1 / τ).im ≤ 0 := by
  rw [neg_div, neg_im, one_div, inv_im, neg_nonpos]
  exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)

Result:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Proof state:
case inr
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
calc
_ = ∑' n : ℤ, cexp (-π * (-I * τ) * ↑n ^ 2 + 2 * π * (I * z) * ↑n) :=
  tsum_congr (fun n ↦ by ring_nf)
_ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * ∑' (n : ℤ), cexp (-π / (-I * τ) * (n + I * (I * z)) ^ 2) := by
  rw [tsum_exp_neg_quadratic h2]
_ = 1 / (-I * τ) ^ (1 / 2 : ℂ) * cexp (π * I * (-1 / τ) * z ^ 2) *
    ∑' (n : ℤ), cexp (2 * π * I * n * (z / τ) + π * I * n ^ 2 * (-1 / τ)) := by
  simp_rw [mul_assoc _ (cexp _), ← tsum_mul_left (a := cexp _), ← Complex.exp_add]
  congr 2 with n : 1; congr 1
  field_simp [I_ne_zero]
  ring_nf
  simp_rw [I_sq, I_pow_four]
  ring_nf
_ = _ := by
  congr 3
  ring

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    1 / (-I * τ) ^ (1 / 2) *
      ∑' (x : ℤ), cexp (↑π * I * (-1 / τ) * z ^ 2 + (2 * ↑π * I * ↑x * (z / τ) + ↑π * I * ↑x ^ 2 * (-1 / τ)))

Tactic:
congr 2 with n : 1

Result:
case e_a.e_f.h
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    cexp (↑π * I * (-1 / τ) * z ^ 2 + (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ)))

Proof state:
case e_a.e_f.h
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2) =
    cexp (↑π * I * (-1 / τ) * z ^ 2 + (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ)))

Tactic:
congr 1

Result:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ -↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2 =
    ↑π * I * (-1 / τ) * z ^ 2 + (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Proof state:
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) = cexp (-↑π * (-I * τ) * ↑n ^ 2 + 2 * ↑π * (I * z) * ↑n)

Tactic:
ring_nf

Result:
no goals

Proof state:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 ≤ -τ.im / normSq τ

Tactic:
exact div_nonneg (neg_nonneg.mpr hτ) (normSq_nonneg τ)

Result:
no goals

Proof state:
z τ : ℂ
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
rcases le_or_lt (im τ) 0 with hτ | hτ

Result:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Proof state:
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ ∑' (n : ℤ), cexp (-↑π * (-I * τ) * ↑n ^ 2 + 2 * ↑π * (I * z) * ↑n) =
    1 / (-I * τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * τ) * (↑n + I * (I * z)) ^ 2)

Tactic:
rw [tsum_exp_neg_quadratic h2]

Result:
no goals

Proof state:
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ 1 / (-I * τ) ^ (1 / 2) * cexp (↑π * I * (-1 / τ) * z ^ 2) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
congr 3

Result:
case e_a.e_a.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ ↑π * I * (-1 / τ) * z ^ 2 = -↑π * I * z ^ 2 / τ

Proof state:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
this : (-1 / τ).im ≤ 0
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
rw [jacobiTheta₂_undef z hτ, jacobiTheta₂_undef _ this, mul_zero]

Result:
no goals

Proof state:
case e_a.e_f.h.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
n : ℤ
⊢ ↑π * ↑n * -1 * z * τ ^ 2 * 2 + ↑π * ↑n ^ 2 * τ ^ 2 + ↑π * 1 * z ^ 2 * τ ^ 2 =
    ↑π * ↑n * -1 * z * τ ^ 2 * 2 + (-(↑π * ↑n ^ 2 * -1 * τ ^ 2) - ↑π * -1 * z ^ 2 * τ ^ 2)

Tactic:
ring_nf

Result:
no goals

Proof state:
case inr
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
⊢ ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Tactic:
have h2 : 0 < (-I * τ).re := by
  simpa only [neg_mul, neg_re, mul_re, I_re, zero_mul, I_im, one_mul, zero_sub, neg_neg] using hτ

Result:
case inr
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * z + ↑π * I * ↑n ^ 2 * τ) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) *
      ∑' (n : ℤ), cexp (2 * ↑π * I * ↑n * (z / τ) + ↑π * I * ↑n ^ 2 * (-1 / τ))

Proof state:
case e_a.e_a.e_z
z τ : ℂ
hτ : 0 < τ.im
h0 : τ ≠ 0
h2 : 0 < (-I * τ).re
⊢ ↑π * I * (-1 / τ) * z ^ 2 = -↑π * I * z ^ 2 / τ

Tactic:
ring

Result:
no goals