Theorems · Theorem · number theory

hasSum_one_div_nat_pow_mul_sin

∀ {k : ℕ},
  k ≠ 0 →
    ∀ {x : ℝ},
      x ∈ Set.Icc 0 1 →
        HasSum (fun n => 1 / ↑n ^ (2 * k + 1) * Real.sin (2 * Real.pi * ↑n * x))
          ((-1) ^ (k + 1) * (2 * Real.pi) ^ (2 * k + 1) / 2 / ↑(2 * k + 1).factorial *
            Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k + 1))))

Defined in

Mathlib.NumberTheory.ZetaValues

Cited by

2 results in Mathlib

Foundations

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