-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Formula for `completedSinZeta` as a Dirichlet series in the convergence range
(first version, with sum over `ℤ`). -/
lemma hasSum_int_completedSinZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℤ ↦ Gammaℝ (s + 1) * (-I) * Int.sign n *
    cexp (2 * π * I * a * n) / (↑|n| : ℂ) ^ s / 2) (completedSinZeta a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
have hF t (ht : 0 < t) :
    HasSum (fun n ↦ c n * n * rexp (-π * n ^ 2 * t)) (sinKernel a t / 2) := by
  refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_
  rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖c n‖ = 1 / 2

Tactic:
simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
  RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re
n : ℤ
⊢ -((s + 1).Gammaℝ * I * ↑(SignType.sign n) * cexp (2 * ↑π * I * ↑a * ↑n)) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * c n * ↑(SignType.sign n) / ↑|n| ^ s

Tactic:
ring

Result:
no goals

Proof state:
case h
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i => 1 / |↑i| ^ s.re

Tactic:
apply Summable.of_nat_of_neg <;>
simpa

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
have hc (n : ℤ) : ‖c n‖ = 1 / 2 := by
  simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
    RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = 2 * ↑π * ↑a * ↑n * I

Tactic:
ring

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i => ‖c i‖ / |↑i| ^ s.re

Tactic:
simp_rw [hc, div_right_comm]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ Summable fun i => 1 / |↑i| ^ s.re / 2

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)

Tactic:
refine ((hasSum_int_sinKernel a ht).div_const 2).congr_fun fun n ↦ ?_

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t)) = -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) / 2

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re
n : ℤ
⊢ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * c n * ↑(SignType.sign ↑n) / ↑|↑n| ^ s

Tactic:
simp [Int.sign_eq_sign, ← Int.cast_abs]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re
n : ℤ
⊢ -((s + 1).Gammaℝ * I * ↑(SignType.sign n) * cexp (2 * ↑π * I * ↑a * ↑n)) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * c n * ↑(SignType.sign n) / ↑|n| ^ s

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = ↑(2 * π * a * ↑n) * I

Tactic:
push_cast

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ 2 * ↑π * I * ↑a * ↑n = 2 * ↑π * ↑a * ↑n * I

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
have h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re := by
  simp_rw [hc, div_right_comm]
  apply Summable.div_const
  apply Summable.of_nat_of_neg <;>
  simpa

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re
⊢ HasSum (fun n => (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
refine (mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum).congr_fun
  fun n ↦ ?_

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i => ‖c i‖ / |↑i| ^ s.re
n : ℤ
⊢ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 =
    (s + 1).Gammaℝ * c n * ↑(SignType.sign ↑n) / ↑|↑n| ^ s

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n => -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t)) = -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) / 2

Tactic:
rw [div_mul_eq_mul_div, div_mul_eq_mul_div, mul_right_comm (-I)]

Result:
no goals