-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
lemma hasSum_int_oddKernel (a : ℝ) {x : ℝ} (hx : 0 < x) :
    HasSum (fun n : ℤ ↦ (n + a) * rexp (-π * (n + a) ^ 2 * x)) (oddKernel ↑a x)

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ (↑n + ↑a) * cexp (-↑π * (↑n + ↑a) ^ 2 * ↑x) =
    (↑n + ↑a) * cexp ((-↑π * ↑a ^ 2 + (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2) * I) * ↑x)

Tactic:
congrm _ * cexp (?_ * x)

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ -↑π * (↑n + ↑a) ^ 2 = -↑π * ↑a ^ 2 + (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2) * I

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
⊢ HasSum (fun x_1 => ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))

Tactic:
have h2 := hasSum_jacobiTheta₂'_term (a * I * x) (by rwa [I_mul_im, ofReal_re])

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
⊢ HasSum (fun x_1 => ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x))

Tactic:
rw [jacobiTheta₂'_term, mul_assoc (2 * π * I), mul_div_cancel_left₀ _ two_pi_I_ne_zero, ← add_mul,
  mul_left_comm, jacobiTheta₂_term, ← Complex.exp_add]

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ -↑π * (↑n + ↑a) ^ 2 = -↑π * ↑a ^ 2 + (2 * ↑π * ↑n * ↑a * -1 + ↑π * ↑n ^ 2 * -1)

Tactic:
ring_nf

Result:
no goals

Proof state:
a x : ℝ
hx : 0 < x
⊢ HasSum (fun x_1 => ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))

Tactic:
have h1 := hasSum_jacobiTheta₂_term (a * I * x) (by rwa [I_mul_im, ofReal_re])

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
⊢ HasSum (fun x_1 => ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ (↑n + ↑a) * cexp (-↑π * (↑n + ↑a) ^ 2 * ↑x) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))

Tactic:
simp only [← mul_assoc, ← add_mul]

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ (↑n + ↑a) * cexp (-↑π * (↑n + ↑a) ^ 2 * ↑x) =
    (↑n + ↑a) * cexp ((-↑π * ↑a ^ 2 + (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2) * I) * ↑x)

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
⊢ HasSum (fun x_1 => ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))

Tactic:
refine (((h2.div_const (2 * π * I)).add (h1.mul_left ↑a)).mul_left
  (cexp (-π * a ^ 2 * x))).congr_fun (fun n ↦ ?_)

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x))

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ -↑π * (↑n + ↑a) ^ 2 = -↑π * ↑a ^ 2 + (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2) * I

Tactic:
simp only [mul_right_comm _ I, add_mul, mul_assoc _ I, I_mul_I]

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ -↑π * (↑n + ↑a) ^ 2 = -↑π * ↑a ^ 2 + (2 * ↑π * ↑n * ↑a * -1 + ↑π * ↑n ^ 2 * -1)

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ ↑((↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))

Tactic:
push_cast

Result:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
h2 : HasSum (fun n => jacobiTheta₂'_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x))
n : ℤ
⊢ (↑n + ↑a) * cexp (-↑π * (↑n + ↑a) ^ 2 * ↑x) =
    (↑n + ↑a) * cexp (-↑π * ↑a ^ 2 * ↑x + (2 * ↑π * I * ↑n * (↑a * I * ↑x) + ↑π * I * ↑n ^ 2 * (I * ↑x)))

Proof state:
a x : ℝ
hx : 0 < x
h1 : HasSum (fun n => jacobiTheta₂_term n (↑a * I * ↑x) (I * ↑x)) (jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))
⊢ 0 < im ?m.81053

Tactic:
rwa [I_mul_im, ofReal_re]

Result:
no goals

Proof state:
a x : ℝ
hx : 0 < x
⊢ HasSum (fun n => (↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) (oddKernel (↑a) x)

Tactic:
rw [← hasSum_ofReal, oddKernel_def' a x]

Result:
a x : ℝ
hx : 0 < x
⊢ HasSum (fun x_1 => ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x)))
    (cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))

Proof state:
a x : ℝ
hx : 0 < x
⊢ 0 < im ?m.80841

Tactic:
rwa [I_mul_im, ofReal_re]

Result:
no goals