-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
theorem sinZeta_two_mul_nat_add_one (hk : k ≠ 0) (hx : x ∈ Icc 0 1) :
    sinZeta x (2 * k + 1) = (-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / (2 * k + 1)! *
      ((Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ)).eval (x : ℂ)

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ (algebraMap ℂ ℂ).comp ofRealHom = ofRealHom.comp (algebraMap ℝ ℝ)

Tactic:
simp

Result:
no goals

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < 2 * k + 1

Tactic:
omega

Result:
no goals

Proof state:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ Real.sin (2 * π * x * ↑n) / ↑(n ^ (2 * k + 1)) = 1 / ↑(n ^ (2 * k + 1)) * Real.sin (2 * π * ↑n * x)

Tactic:
ring_nf

Result:
no goals

Proof state:
case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ ofRealHom (Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    Polynomial.eval (ofRealHom x)
      (Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Tactic:
apply Polynomial.map_aeval_eq_aeval_map (by simp)

Result:
no goals

Proof state:
case refine_2
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
congr 1

Result:
case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Proof state:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) =
    ∑' (a : ℕ), ↑(1 / ↑a ^ (2 * k + 1) * Real.sin (2 * π * ↑a * x))

Tactic:
refine tsum_congr fun n ↦ ?_

Result:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(Real.sin (2 * π * x * ↑n)) / ↑n ^ (2 * ↑k + 1) = ↑(1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))

Proof state:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) =
    ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k + 1) * Real.sin (2 * π * ↑b * x))

Tactic:
rw [ofReal_tsum]

Result:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) =
    ∑' (a : ℕ), ↑(1 / ↑a ^ (2 * k + 1) * Real.sin (2 * π * ↑a * x))

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k + 1).re

Tactic:
norm_cast

Result:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < 2 * k + 1

Proof state:
case refine_2
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
push_cast

Result:
case refine_2
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Proof state:
case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
have : (Polynomial.bernoulli (2 * k + 1)).map (algebraMap ℚ ℂ) = _ :=
  (Polynomial.map_map (algebraMap ℚ ℝ) ofRealHom _).symm

Result:
case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Proof state:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(Real.sin (2 * π * x * ↑n)) / ↑n ^ (2 * ↑k + 1) = ↑(1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))

Tactic:
norm_cast

Result:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ Real.sin (2 * π * x * ↑n) / ↑(n ^ (2 * k + 1)) = 1 / ↑(n ^ (2 * k + 1)) * Real.sin (2 * π * ↑n * x)

Proof state:
case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ ↑(Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
rw [this, ← ofRealHom_eq_coe, ← ofRealHom_eq_coe]

Result:
case refine_2.e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this :
  Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)) =
    Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))
⊢ ofRealHom (Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    Polynomial.eval (ofRealHom x)
      (Polynomial.map ofRealHom (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
refine Eq.trans ?_ <|
  (congr_arg ofReal (hasSum_one_div_nat_pow_mul_sin hk hx).tsum_eq).trans ?_

Result:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) =
    ↑(∑' (b : ℕ), 1 / ↑b ^ (2 * k + 1) * Real.sin (2 * π * ↑b * x))

case refine_2
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ↑((-1) ^ (k + 1) * (2 * π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
        Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1)))) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Proof state:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ sinZeta (↑x) (2 * ↑k + 1) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
rw [← (hasSum_nat_sinZeta x (?_ : 1 < re (2 * k + 1))).tsum_eq]

Result:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ ∑' (b : ℕ), ↑(Real.sin (2 * π * x * ↑b)) / ↑b ^ (2 * ↑k + 1) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! *
      Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k + 1).re