-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
lemma evenKernel_functional_equation (a : UnitAddCircle) (x : ℝ) :
    evenKernel a x = 1 / x ^ (1 / 2 : ℝ) * cosKernel a (1 / x)

Proof state:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Tactic:
have h2 : a * I * x / (I * x) = a := by
  rw [div_eq_iff hx']
  ring

Result:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Proof state:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Tactic:
rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
  ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]

Result:
no goals

Proof state:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
⊢ evenKernel (↑a) x = 1 / x ^ (1 / 2) * cosKernel (↑a) (1 / x)

Tactic:
rw [← ofReal_inj, ofReal_mul, evenKernel_def, cosKernel_def, jacobiTheta₂_functional_equation]

Result:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Proof state:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
⊢ -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)

Tactic:
rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']

Result:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
⊢ -↑π * I * (↑a ^ 2 * -1 * ↑x ^ 2) = -(-↑π * ↑a ^ 2 * ↑x) * (I * ↑x)

Proof state:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
⊢ ↑a * I * ↑x = ↑a * (I * ↑x)

Tactic:
ring

Result:
no goals

Proof state:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Tactic:
have h1 : I * ↑(1 / x) = -1 / (I * x) := by
  push_cast
  rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]

Result:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Proof state:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (1 / ↑x) = -1 / (I * ↑x)

Tactic:
rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]

Result:
no goals

Proof state:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Tactic:
have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = - (-π * a ^ 2 * x) := by
  rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
  ring

Result:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
h3 : 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))
h4 : -↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x) = -(-↑π * ↑a ^ 2 * ↑x)
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Proof state:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Tactic:
have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')

Result:
case inr.H
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
⊢ cexp (-↑π * ↑a ^ 2 * ↑x) *
      (1 / (-I * (I * ↑x)) ^ (1 / 2) * cexp (-↑π * I * (↑a * I * ↑x) ^ 2 / (I * ↑x)) *
        jacobiTheta₂ (↑a * I * ↑x / (I * ↑x)) (-1 / (I * ↑x))) =
    ↑(1 / x ^ (1 / 2)) * jacobiTheta₂ (↑a) (I * ↑(1 / x))

Proof state:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
⊢ ↑a * I * ↑x / (I * ↑x) = ↑a

Tactic:
rw [div_eq_iff hx']

Result:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
⊢ ↑a * I * ↑x = ↑a * (I * ↑x)

Proof state:
case inl.hx
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 1 / x ≤ 0

Tactic:
exact div_nonpos_of_nonneg_of_nonpos zero_le_one hx

Result:
no goals

Proof state:
case inr
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a =>
rw [← ofReal_inj, ofReal_mul, evenKernel_def, cosKernel_def, jacobiTheta₂_functional_equation]
have h1 : I * ↑(1 / x) = -1 / (I * x) := by
  push_cast
  rw [← div_div, mul_one_div, div_I, neg_one_mul, neg_neg]
have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')
have h2 : a * I * x / (I * x) = a := by
  rw [div_eq_iff hx']
  ring
have h3 : 1 / (-I * (I * x)) ^ (1 / 2 : ℂ) = 1 / ↑(x ^ (1 / 2 : ℝ)) := by
  rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg,ofReal_cpow hx.le, ofReal_div,
    ofReal_one, ofReal_ofNat]
have h4 : -π * I * (a * I * x) ^ 2 / (I * x) = - (-π * a ^ 2 * x) := by
  rw [mul_pow, mul_pow, I_sq, div_eq_iff hx']
  ring
rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
  ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * ↑(1 / x) = -1 / (I * ↑x)
hx' : I * ↑x ≠ 0
h2 : ↑a * I * ↑x / (I * ↑x) = ↑a
⊢ 1 / (-I * (I * ↑x)) ^ (1 / 2) = 1 / ↑(x ^ (1 / 2))

Tactic:
rw [neg_mul, ← mul_assoc, I_mul_I, neg_one_mul, neg_neg,ofReal_cpow hx.le, ofReal_div,
  ofReal_one, ofReal_ofNat]

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * ↑(1 / x) = -1 / (I * ↑x)

Tactic:
push_cast

Result:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (1 / ↑x) = -1 / (I * ↑x)

Proof state:
case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
rw [evenKernel_undef _ hx, cosKernel_undef, mul_zero]

Result:
case inl.hx
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 1 / x ≤ 0