-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Formula for `completedHurwitzZetaOdd` as a Dirichlet series in the convergence range. -/
lemma hasSum_int_completedHurwitzZetaOdd (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℤ ↦ Gammaℝ (s + 1) * SignType.sign (n + a) / (↑|n + a| : ℂ) ^ s / 2)
    (completedHurwitzZetaOdd a s)

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)

Tactic:
let r (n : ℤ) : ℝ := n + a

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n => ↑n + a
⊢ HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)

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

Tactic:
rwa [summable_one_div_int_add_rpow]

Result:
no goals

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

Tactic:
have := mellin_div_const .. ▸ hasSum_mellin_pi_mul_sq' (zero_lt_one.trans hs) hF h_sum

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

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

Tactic:
apply Summable.mul_left

Result:
case hf
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n => ↑n + a
c : ℤ → ℂ := fun n => 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)
⊢ Summable fun i => 1 / |r i| ^ s.re

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

Tactic:
refine this.congr_fun fun n ↦ ?_

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

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n => ↑n + a
⊢ HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)

Tactic:
let c (n : ℤ) : ℂ := 1 / 2

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n => ↑n + a
c : ℤ → ℂ := fun n => 1 / 2
⊢ HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)

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

Tactic:
simp_rw [c, ← mul_one_div ‖_‖]

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

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

Tactic:
have h_sum : Summable fun i ↦ ‖c i‖ / |r i| ^ s.re := by
  simp_rw [c, ← mul_one_div ‖_‖]
  apply Summable.mul_left
  rwa [summable_one_div_int_add_rpow]

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

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

Tactic:
simp [r, c, push_cast, div_mul_eq_mul_div, -one_div]

Result:
no goals

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

Tactic:
simp only [r, c, mul_one_div, div_mul_eq_mul_div, div_right_comm]

Result:
no goals

Proof state:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n => ↑n + a
c : ℤ → ℂ := fun n => 1 / 2
t : ℝ
ht : 0 < t
⊢ HasSum (fun n => c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)

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

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

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

Tactic:
have hF t (ht : 0 < t) : HasSum (fun n ↦ c n * r n * rexp (-π * (r n) ^ 2 * t))
    (oddKernel a t / 2) := by
  refine ((hasSum_ofReal.mpr (hasSum_int_oddKernel a ht)).div_const 2).congr_fun fun n ↦ ?_
  simp [r, c, push_cast, div_mul_eq_mul_div, -one_div]

Result:
a : ℝ
s : ℂ
hs : 1 < s.re
r : ℤ → ℝ := fun n => ↑n + a
c : ℤ → ℂ := fun n => 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => c n * ↑(r n) * ↑(rexp (-π * r n ^ 2 * t))) (↑(oddKernel (↑a) t) / 2)
⊢ HasSum (fun n => (s + 1).Gammaℝ * ↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s / 2) (completedHurwitzZetaOdd (↑a) s)