English
There is a recurrence relation for bernoulliFourierCoeff in k, relating bernoulliFourierCoeff(k) to bernoulliFourierCoeff(k−1) via a rational factor involving π and i.
Русский
Существует реккурентное соотношение коэффициентов bernoulliFourierCoeff по k, связывающее bernoulliFourierCoeff(k) с bernoulliFourierCoeff(k−1) через рациональный множитель, включающий π и i.
LaTeX
$$$$ bernoulliFourierCoeff(k,n) = \\frac{1}{-2\\pi i n} \\left(\\mathbf{1}_{k=1} - k\\, bernoulliFourierCoeff(k-1,n)\\right). $$$$
Lean4
/-- Recurrence relation (in `k`) for the `n`-th Fourier coefficient of `Bₖ`. -/
theorem bernoulliFourierCoeff_recurrence (k : ℕ) {n : ℤ} (hn : n ≠ 0) :
bernoulliFourierCoeff k n = 1 / (-2 * π * I * n) * (ite (k = 1) 1 0 - k * bernoulliFourierCoeff (k - 1) n) :=
by
unfold bernoulliFourierCoeff
rw [fourierCoeffOn_of_hasDerivAt zero_lt_one hn (fun x _ => (hasDerivAt_bernoulliFun k x).ofReal_comp)
((continuous_ofReal.comp <| continuous_const.mul <| Polynomial.continuous _).intervalIntegrable _ _)]
simp_rw [ofReal_one, ofReal_zero, sub_zero, one_mul]
rw [QuotientAddGroup.mk_zero, fourier_eval_zero, one_mul, ← ofReal_sub, bernoulliFun_eval_one, add_sub_cancel_left]
congr 2
· split_ifs <;> simp only [ofReal_one, ofReal_zero]
· simp_rw [ofReal_mul, ofReal_natCast, fourierCoeffOn.const_mul]
