Theorems · Theorem · number theory

HurwitzZeta.hasSum_nat_completedCosZeta

∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum (fun n => if n = 0 then 0 else s.Gammaℝ * ↑(Real.cos (2 * Real.pi * a * ↑n)) / ↑n ^ s)
      (HurwitzZeta.completedCosZeta (↑a) s)

Formula for completedCosZeta as a Dirichlet series in the convergence range (second version, with sum over ℕ).

Defined in: Mathlib.NumberTheory.LSeries.HurwitzZetaEven
Cited by: 1 results in Mathlib
Foundations: Depth 302 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites38

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
Complexstatement and proof · cited by 5,565
add_zeroproof · cited by 2,707
zero_addproof · cited by 2,366
SummationFilter.unconditionalstatement and proof · cited by 2,068
Nat.cast_zeroproof · cited by 1,870
absproof · cited by 1,814
Real.pistatement and proof · cited by 1,774
Complex.ofRealstatement and proof · cited by 1,654
Complex.restatement and proof · cited by 882
Complex.Iproof · cited by 866
neg_mulproof · cited by 654

Cited by1

Results whose statement or proof uses this declaration.

completedZeta_eq_tsum_of_one_lt_reproof · cited by 0