awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
this : cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)
rw :
  rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x + π * (x + 2 * ξ * x)) *
      (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
    rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re
⊢ rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x) *
      (cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) *
          jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
    rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re

Tactic:
rw [this, re_ofReal_mul, ← mul_assoc, ← Real.exp_add]

Premises used: mul_assoc, Real.exp_add, Complex.re_ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
this : cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)
e_a : -π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x + π * (x + 2 * ξ * x) = -π * HPow.hPow (β := ℕ) ξ 2 * x
⊢ rexp (-π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x + π * (x + 2 * ξ * x)) *
      (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re =
    rexp (-π * HPow.hPow (β := ℕ) ξ 2 * x) * (jacobiTheta₂ ((↑ξ : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))).re

Tactic:
congr
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
this : cexp (-(↑π : ℂ) * I * (I * (↑x : ℂ) + 2 * ((↑ξ : ℂ) * I * (↑x : ℂ)))) = (↑(rexp (π * (x + 2 * ξ * x))) : ℂ)
⊢ -π * HPow.hPow (β := ℕ) (ξ + 1) 2 * x + π * (x + 2 * ξ * x) = -π * HPow.hPow (β := ℕ) ξ 2 * x

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a x : ℝ
⊢ (↑(evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) =
    cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) * jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))

Tactic:
simp [evenKernel, re_eq_add_conj, jacobiTheta₂_conj, ← mul_two,
    mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

Premises used: jacobiTheta₂_conj, Complex.re_eq_add_conj, HurwitzZeta.evenKernel, mul_div_cancel_right₀, two_ne_zero', Complex, mul_two
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ (I * (↑x : ℂ)).im ≤ 0

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : x ≤ 0
a' : ℝ
⊢ evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0

Tactic:
simp [← ofReal_inj, evenKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Premises used: HurwitzZeta.evenKernel_def, jacobiTheta₂_undef, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
H : ∀ (a' : ℝ), evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
⊢ evenKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H a' => simp [← ofReal_inj, evenKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Premises used: HurwitzZeta.evenKernel_def, jacobiTheta₂_undef, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x ξ : ℝ
⊢ Eq (α := ℝ) ((fun (ξ : ℝ) ↦ (jacobiTheta₂ (↑ξ : ℂ) (I * (↑x : ℂ))).re) (ξ + 1))
    ((fun (ξ : ℝ) ↦ (jacobiTheta₂ (↑ξ : ℂ) (I * (↑x : ℂ))).re) ξ)

Tactic:
simp [jacobiTheta₂_add_left]

Premises used: jacobiTheta₂_add_left
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a x : ℝ
⊢ (↑(cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ) = jacobiTheta₂ (↑a : ℂ) (I * (↑x : ℂ))

Tactic:
simp [cosKernel, re_eq_add_conj, jacobiTheta₂_conj, ← mul_two,
    mul_div_cancel_right₀ _ (two_ne_zero' ℂ)]

Premises used: jacobiTheta₂_conj, Complex.re_eq_add_conj, HurwitzZeta.cosKernel, mul_div_cancel_right₀, two_ne_zero', Complex, mul_two
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : x ≤ 0
z : ℝ
⊢ (I * (↑x : ℂ)).im ≤ 0

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : x ≤ 0
z : ℝ
⊢ cosKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0

Tactic:
simp [← ofReal_inj, cosKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Premises used: jacobiTheta₂_undef, HurwitzZeta.cosKernel_def, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
H : ∀ (z : ℝ), cosKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x = 0
⊢ cosKernel a x = 0

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H => simp [← ofReal_inj, cosKernel_def, jacobiTheta₂_undef _ (by simpa : (I * ↑x).im ≤ 0)]

Premises used: jacobiTheta₂_undef, HurwitzZeta.cosKernel_def, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
h : ∀ (x : ℝ), evenKernel 0 x = cosKernel 0 x
⊢ evenKernel 0 = cosKernel 0

Tactic:
ext1 x
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
⊢ evenKernel 0 x = cosKernel 0 x

Tactic:
simp [← QuotientAddGroup.mk_zero, ← ofReal_inj, evenKernel_def, cosKernel_def]

Premises used: HurwitzZeta.evenKernel_def, QuotientAddGroup.mk_zero, HurwitzZeta.cosKernel_def, Complex.ofReal_inj
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x z : ℝ
⊢ evenKernel (-(↑z : ℝ ⧸ AddSubgroup.zmultiples 1)) x = evenKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x

Tactic:
simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

Premises used: HurwitzZeta.evenKernel_def, jacobiTheta₂_neg_left, Complex.ofReal_inj, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
H : ∀ (z : ℝ), evenKernel (-(↑z : ℝ ⧸ AddSubgroup.zmultiples 1)) x = evenKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x
⊢ evenKernel (-a) x = evenKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, evenKernel_def, jacobiTheta₂_neg_left]

Premises used: HurwitzZeta.evenKernel_def, jacobiTheta₂_neg_left, Complex.ofReal_inj, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x z : ℝ
⊢ cosKernel (-(↑z : ℝ ⧸ AddSubgroup.zmultiples 1)) x = cosKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x

Tactic:
simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]

Premises used: HurwitzZeta.cosKernel_def, Complex.ofReal_inj, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
H : ∀ (z : ℝ), cosKernel (-(↑z : ℝ ⧸ AddSubgroup.zmultiples 1)) x = cosKernel (↑z : ℝ ⧸ AddSubgroup.zmultiples 1) x
⊢ cosKernel (-a) x = cosKernel a x

Tactic:
induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]

Premises used: HurwitzZeta.cosKernel_def, Complex.ofReal_inj, QuotientAddGroup.mk_neg
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' : ℝ
H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
⊢ ContinuousOn (evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)

Tactic:
apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))

Premises used: Continuous.comp_continuousOn, Complex.continuous_re
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' : ℝ
H :
  ContinuousOn (Y := ℂ)
    (fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a' : ℂ) 2 * (↑x : ℂ)) *
        jacobiTheta₂ ((↑a' : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (Ioi 0)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)

Tactic:
simp only [evenKernel_def]

Premises used: HurwitzZeta.evenKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a' : ℂ) 2 * (↑x : ℂ))) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' : ℝ
H :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ ((↑a' : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) x
⊢ ContinuousOn (Y := ℂ)
    (fun (x : ℝ) ↦
      cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a' : ℂ) 2 * (↑x : ℂ)) *
        jacobiTheta₂ ((↑a' : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ)))
    (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)

Premises used: continuousOn_of_forall_continuousAt, ContinuousAt.mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ 0 < (I * (↑x : ℂ)).im

Tactic:
simpa
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (u : ℝ) ↦ ((↑a' : ℂ) * I * (↑u : ℂ), I * (↑u : ℂ))) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ ((↑a' : ℂ) * I * (↑x : ℂ)) (I * (↑x : ℂ))) x

Tactic:
exact (continuousAt_jacobiTheta₂ (a' * I * x) <| by simpa).comp
    (f := fun u : ℝ ↦ (a' * I * u, I * u)) (by fun_prop)

Premises used: HMul.hMul, Complex.ofReal, continuousAt_jacobiTheta₂, ContinuousAt.comp, Complex.I
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
H : ∀ (a' : ℝ), ContinuousOn (evenKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
⊢ ContinuousOn (evenKernel a) (Ioi 0)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a' =>
  apply continuous_re.comp_continuousOn (f := fun x ↦ (evenKernel a' x : ℂ))
  simp only [evenKernel_def]
  refine continuousOn_of_forall_continuousAt (fun x hx ↦ .mul (by fun_prop) ?_)
  exact (continuousAt_jacobiTheta₂ (a' * I * x) <| by simpa).comp
    (f := fun u : ℝ ↦ (a' * I * u, I * u)) (by fun_prop)

Premises used: HurwitzZeta.evenKernel_def, continuousOn_of_forall_continuousAt, ContinuousAt.mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' : ℝ
H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)
⊢ ContinuousOn (cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)

Tactic:
apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))

Premises used: Continuous.comp_continuousOn, Complex.continuous_re
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' : ℝ
H : ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) (Ioi 0)
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ (↑(cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1) x) : ℂ)) (Ioi 0)

Tactic:
simp only [cosKernel_def]

Premises used: HurwitzZeta.cosKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' : ℝ
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) (Ioi 0)

Tactic:
continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' : ℝ
H :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioi 0) x),
    ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) x
⊢ ContinuousOn (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) (Ioi 0)

Tactic:
refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)

Premises used: continuousOn_of_forall_continuousAt
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ × ℂ) (fun (u : ℝ) ↦ ((↑a' : ℂ), I * (↑u : ℂ))) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a' x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioi 0) x
⊢ ContinuousAt (Y := ℂ) (fun (x : ℝ) ↦ jacobiTheta₂ (↑a' : ℂ) (I * (↑x : ℂ))) x

Tactic:
exact (continuousAt_jacobiTheta₂ a' <| by simpa).comp
    (f := fun u : ℝ ↦ ((a' : ℂ), I * u)) (by fun_prop)

Premises used: Complex.ofReal, continuousAt_jacobiTheta₂, ContinuousAt.comp
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
H : ∀ (a' : ℝ), ContinuousOn (cosKernel (↑a' : ℝ ⧸ AddSubgroup.zmultiples 1)) (Ioi 0)
⊢ ContinuousOn (cosKernel a) (Ioi 0)

Tactic:
induction a using QuotientAddGroup.induction_on with | H a' =>
  apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))
  simp only [cosKernel_def]
  refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)
  exact (continuousAt_jacobiTheta₂ a' <| by simpa).comp
    (f := fun u : ℝ ↦ ((a' : ℂ), I * u)) (by fun_prop)

Premises used: continuousOn_of_forall_continuousAt, HurwitzZeta.cosKernel_def
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
inl : ∀ (hx : x ≤ 0), evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
inr : ∀ (hx : 0 < x), evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
rcases le_or_gt x 0 with hx | hx

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
inl : 1 / x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

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

Premises used: MulZeroClass.mul_zero, HurwitzZeta.cosKernel_undef, HurwitzZeta.evenKernel_undef
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 1 / x ≤ 0

Tactic:
div_nonpos_of_nonneg_of_nonpos zero_le_one hx

Premises used: div_nonpos_of_nonneg_of_nonpos, zero_le_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ 1 / x ≤ 0

Tactic:
exact div_nonpos_of_nonneg_of_nonpos zero_le_one hx

Premises used: div_nonpos_of_nonneg_of_nonpos, zero_le_one
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
inr :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
⊢ evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
    1 / x ^ (1 / 2) * cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / x)

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

Premises used: jacobiTheta₂_functional_equation, HurwitzZeta.evenKernel_def, HurwitzZeta.cosKernel_def, Complex.ofReal_inj, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
push_cast : I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))
⊢ I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))

Tactic:
push_cast
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
rw : I * (1 / (↑x : ℂ)) = -1 / I / (↑x : ℂ)
rw₁ : I / (↑x : ℂ) = -1 / I / (↑x : ℂ)
rw₂ : I / (↑x : ℂ) = -(-1 * I) / (↑x : ℂ)
rw₃ : I / (↑x : ℂ) = - -I / (↑x : ℂ)
rw₄ rw₅ : I / (↑x : ℂ) = I / (↑x : ℂ)
⊢ I * (1 / (↑x : ℂ)) = -1 / (I * (↑x : ℂ))

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

Premises used: neg_one_mul, neg_neg, mul_one_div, Complex.div_I, div_div
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
⊢ I * (↑(1 / x) : ℂ) = -1 / (I * (↑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]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
⊢ I * (↑x : ℂ) ≠ 0

Tactic:
have hx' : I * x ≠ 0 := mul_ne_zero I_ne_zero (ofReal_ne_zero.mpr hx.ne')
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
rw : (↑a : ℂ) * I * (↑x : ℂ) = (↑a : ℂ) * (I * (↑x : ℂ))
⊢ (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)

Tactic:
rw [div_eq_iff hx']

Premises used: div_eq_iff
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
⊢ (↑a : ℂ) * I * (↑x : ℂ) = (↑a : ℂ) * (I * (↑x : ℂ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
⊢ (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)

Tactic:
have h2 : a * I * x / (I * x) = a := by
    rw [div_eq_iff hx']
    ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
rw : 1 / (-(I * (I * (↑x : ℂ)))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₁ : 1 / (-(I * I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₂ : 1 / (-(-1 * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₃ : 1 / (- -(↑x : ℂ)) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₄ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
rw₅ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (↑(1 / 2) : ℂ)
rw₆ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ ((↑1 : ℂ) / (↑2 : ℂ))
rw₇ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ (1 / (↑2 : ℂ))
rw₈ rw₉ : 1 / (↑x : ℂ) ^ (1 / 2) = 1 / (↑x : ℂ) ^ HDiv.hDiv (α := ℂ) 1 2
⊢ 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]

Premises used: Complex.ofReal_cpow, mul_assoc, neg_one_mul, neg_neg, LT.lt.le, Complex.ofReal_one, Complex.I_mul_I, Complex.ofReal_div, neg_mul, Complex.ofReal_ofNat
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
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:
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]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
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)) : ℂ)
rw :
  -(↑π : ℂ) * I * (HPow.hPow (β := ℕ) (↑a : ℂ) 2 * -1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) * (I * (↑x : ℂ))
⊢ -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))

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

Premises used: div_eq_iff, Complex.I_sq, mul_pow
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
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 * (HPow.hPow (β := ℕ) (↑a : ℂ) 2 * -1 * HPow.hPow (β := ℕ) (↑x : ℂ) 2) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) * (I * (↑x : ℂ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
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 * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑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
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a : UnitAddCircle
x : ℝ
hx : 0 < x
inr :
  ∀ (a : ℝ),
    evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) x =
      1 / x ^ (1 / 2) * cosKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) (1 / 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]

Premises used: jacobiTheta₂_functional_equation, HurwitzZeta.evenKernel_def, Complex.exp_add, Complex.exp_zero, mul_assoc, Complex.ofReal_one, neg_add_cancel, HurwitzZeta.cosKernel_def, mul_comm, Complex.exp, Complex.ofReal_div, Complex.ofReal_inj, mul_one, Complex.ofReal_mul
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
rw :
  HasSum (fun (x : ℤ) ↦ (↑(rexp (-π * HPow.hPow (β := ℕ) ((↑x : ℝ) + a) 2 * t)) : ℂ))
    (cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ)) *
      jacobiTheta₂ ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ)))
⊢ HasSum (fun (n : ℤ) ↦ rexp (-π * HPow.hPow (β := ℕ) ((↑n : ℝ) + a) 2 * t))
    (evenKernel (↑a : ℝ ⧸ AddSubgroup.zmultiples 1) t)

Tactic:
rw [← hasSum_ofReal, evenKernel_def]

Premises used: HurwitzZeta.evenKernel_def, Complex.hasSum_ofReal
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
rw :
  cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
    cexp
      (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ)) +
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑t : ℂ)) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ))))
⊢ cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
    cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ))) *
      jacobiTheta₂_term n ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ))

Tactic:
rw [jacobiTheta₂_term, ← Complex.exp_add]

Premises used: Complex.exp_add, jacobiTheta₂_term
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
n : ℤ
⊢ cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
    cexp
      (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ)) +
        (2 * (↑π : ℂ) * I * (↑n : ℂ) * ((↑a : ℂ) * I * (↑t : ℂ)) +
          (↑π : ℂ) * I * HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 2 * (I * (↑t : ℂ))))

Tactic:
grind [I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
⊢ ∀ (n : ℤ),
    cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
      cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ))) *
        jacobiTheta₂_term n ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ))

Tactic:
have (n : ℤ) : cexp (-(π * (n + a) ^ 2 * t)) = cexp (-(π * a ^ 2 * t)) *
      jacobiTheta₂_term n (a * I * t) (I * t) := by
    rw [jacobiTheta₂_term, ← Complex.exp_add]
    grind [I_sq]
-- Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Goal:
a t : ℝ
ht : 0 < t
this :
  ∀ (n : ℤ),
    cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) ((↑n : ℂ) + (↑a : ℂ)) 2 * (↑t : ℂ))) =
      cexp (-((↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑t : ℂ))) *
        jacobiTheta₂_term n ((↑a : ℂ) * I * (↑t : ℂ)) (I * (↑t : ℂ))
⊢ 0 < (I * (↑t : ℂ)).im

Tactic:
simpa