English
For k ≠ 0 and n ∈ ℤ, the Fourier coefficient of the lifted periodized Bernoulli function is -k!/(2π i n)^k.
Русский
Для k ≠ 0 и n ∈ ℤ фурье-коэффициент функции, полученной путем подъема периодизированной Бернулли, равен $-k!/(2\pi i n)^k$.
LaTeX
$$$\text{fourierCoeff}((\uparrow) \circ periodizedBernoulli(k))\, n = -\dfrac{k!}{(2\pi i n)^k}, \quad n \in \mathbb{Z},\ k \neq 0.$$$
Lean4
theorem fourierCoeff_bernoulli_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) :
fourierCoeff ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) n = -k ! / (2 * π * I * n) ^ k :=
by
have : ((↑) ∘ periodizedBernoulli k : 𝕌 → ℂ) = AddCircle.liftIco 1 0 ((↑) ∘ bernoulliFun k) := by ext1 x; rfl
rw [this, fourierCoeff_liftIco_eq]
simpa only [zero_add] using bernoulliFourierCoeff_eq hk n
