English
For k > 0, bernoulliFourierCoeff k n satisfies a rational expression in n and k involving factorials and π; a closed-form recurrence is given.
Русский
Для k > 0 коэффициенты bernoulliFourierCoeff k n удовлетворяют рациональному выражению в зависимости от n и k, включая факториалы и π; приведена закрытая формула через рекуррентность.
LaTeX
$$$$ bernoulliFourierCoeff(k,n) = -\\frac{k!}{(2\\pi i n)^k} \\quad \\text{(при некоторых условиях на n)} $$$$
Lean4
theorem bernoulliFourierCoeff_eq {k : ℕ} (hk : k ≠ 0) (n : ℤ) :
bernoulliFourierCoeff k n = -k ! / (2 * π * I * n) ^ k :=
by
rcases eq_or_ne n 0 with (rfl | hn)
· rw [bernoulliFourierCoeff_zero hk, Int.cast_zero, mul_zero, zero_pow hk, div_zero]
refine Nat.le_induction ?_ (fun k hk h'k => ?_) k (Nat.one_le_iff_ne_zero.mpr hk)
· rw [bernoulliFourierCoeff_recurrence 1 hn]
simp only [Nat.cast_one, tsub_self, neg_mul, one_mul, if_true, Nat.factorial_one, pow_one]
rw [bernoulli_zero_fourier_coeff hn, sub_zero, mul_one, div_neg, neg_div]
· rw [bernoulliFourierCoeff_recurrence (k + 1) hn, Nat.add_sub_cancel k 1]
split_ifs with h
· exfalso; exact (ne_of_gt (Nat.lt_succ_iff.mpr hk)) h
· rw [h'k, Nat.factorial_succ, zero_sub, Nat.cast_mul, pow_add, pow_one, neg_div, mul_neg, mul_neg, mul_neg,
neg_neg, neg_mul, neg_mul, neg_mul, div_neg]
field_simp
