-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version without absolute values, assuming `a ∈ Icc 0 1`) -/
lemma hasSum_nat_hurwitzZetaOdd_of_mem_Icc {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ (1 / (n + a : ℂ) ^ s - 1 / (n + 1 - a : ℂ) ^ s) / 2)
    (hurwitzZetaOdd a s)

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ ↑n + ↑b = ↑(↑n + b)

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s

Tactic:
rcases lt_or_eq_of_le (by positivity : 0 ≤ n + b) with hb | hb

Result:
case inl
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 < ↑n + b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s

case inr
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 = ↑n + b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s

Proof state:
case inl
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 < ↑n + b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s

Tactic:
simp [sign_pos hb]

Result:
no goals

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
this : ∀ (b : ℝ), 0 ≤ b → ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s
⊢ (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2 =
    (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2

Tactic:
simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]

Result:
no goals

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2 =
    (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2

Tactic:
suffices ∀ b : ℝ, 0 ≤ b → SignType.sign (n + b) / (↑|n + b| : ℂ) ^ s = 1 / (n + b) ^ s by
  simp only [add_sub_assoc, this a ha.1, this (1 - a) (sub_nonneg.mpr ha.2), push_cast]

Result:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ∀ (b : ℝ), 0 ≤ b → ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ 0 ≤ ↑n + b

Tactic:
positivity

Result:
no goals

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2) (hurwitzZetaOdd (↑a) s)

Tactic:
refine (hasSum_nat_hurwitzZetaOdd a hs).congr_fun fun n ↦ ?_

Result:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2 =
    (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ∀ (b : ℝ), 0 ≤ b → ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s

Tactic:
intro b hb

Result:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ ↑(SignType.sign (↑n + b)) / ↑|↑n + b| ^ s = 1 / (↑n + ↑b) ^ s

Tactic:
rw [abs_of_nonneg (by positivity), (by simp : (n : ℂ) + b = ↑(n + b))]

Result:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb : 0 ≤ b
⊢ ↑(SignType.sign (↑n + b)) / ↑(↑n + b) ^ s = 1 / ↑(↑n + b) ^ s