Theorems · Theorem · number theory

HurwitzZeta.hasSum_nat_hurwitzZetaOdd_of_mem_Icc

∀ {a : ℝ},
  a ∈ Set.Icc 0 1 →
    ∀ {s : ℂ},
      1 < s.re → HasSum (fun n => (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2) (HurwitzZeta.hurwitzZetaOdd (↑a) s)

Formula for hurwitzZetaOdd as a Dirichlet series in the convergence range, with sum over ℕ (version without absolute values, assuming a ∈ Icc 0 1)

Defined in

Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Cited by

1 results in Mathlib

Foundations

Depth 306 from the axioms · uses propext, Classical.choice, Quot.sound