Theorems · Theorem · number theory

hasSum_one_div_pow_mul_fourier_mul_bernoulliFun

∀ {k : ℕ},
  2 ≤ k →
    ∀ {x : ℝ},
      x ∈ Set.Icc 0 1 →
        HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑x)
          (-(2 * ↑Real.pi * Complex.I) ^ k / ↑k.factorial * ↑(bernoulliFun k x))

Defined in: Mathlib.NumberTheory.ZetaValues
Cited by: 1 results in Mathlib
Foundations: Depth 276 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.

Cites59

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

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Realstatement and proof · cited by 25,697
TopologicalSpaceproof · cited by 24,529
AddCommMonoidproof · cited by 12,281
Complexstatement and proof · cited by 5,565
ContinuousMapstatement and proof · cited by 2,491
zero_addproof · cited by 2,366
HasQuotient.Quotientproof · cited by 2,301
SummationFilter.unconditionalstatement and proof · cited by 2,068
Real.pistatement and proof · cited by 1,774
Set.Iccstatement and proof · cited by 1,702

Cited by1

Results whose statement or proof uses this declaration.

hasSum_one_div_nat_pow_mul_fourierproof · cited by 2