English
For k ≥ 2 and x ∈ [0,1], the HasSum of the symmetric Fourier series ∑ 1/n^k [fourier(n,x) + (-1)^k fourier(-n,x)] equals -(2π i)^k/k! bernoulliFun(k,x).
Русский
Для k ≥ 2 и x ∈ [0,1] имеет место сумма Фурье с симметрическими слагаемыми: $\sum_{n\ge1} \frac{1}{n^{k}}[\text{fourier}(n,x) + (-1)^k \text{fourier}(-n,x)] = -\frac{(2\pi i)^{k}}{k!} \text{bernoulliFun}(k,x).$
LaTeX
$$$\text{HasSum}\left( \sum_{n=1}^{\infty} \dfrac{1}{n^{k}} \left( \text{fourier}(n,x) + (-1)^{k} \text{fourier}(-n,x) \right) \right) = -\dfrac{(2\pi i)^{k}}{k!} \; \text{bernoulliFun}(k,x).$$$
Lean4
theorem hasSum_one_div_nat_pow_mul_fourier {k : ℕ} (hk : 2 ≤ k) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) :
HasSum (fun n : ℕ => (1 : ℂ) / (n : ℂ) ^ k * (fourier n (x : 𝕌) + (-1 : ℂ) ^ k * fourier (-n) (x : 𝕌)))
(-(2 * π * I) ^ k / k ! * bernoulliFun k x) :=
by
convert (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).nat_add_neg using 1
· ext1 n
rw [Int.cast_neg, mul_add, ← mul_assoc]
conv_rhs => rw [neg_eq_neg_one_mul, mul_pow, ← div_div]
congr 2
rw [div_mul_eq_mul_div₀, one_mul]
congr 1
rw [eq_div_iff, ← mul_pow, ← neg_eq_neg_one_mul, neg_neg, one_pow]
apply pow_ne_zero; rw [neg_ne_zero]; exact one_ne_zero
· rw [Int.cast_zero, zero_pow (by positivity : k ≠ 0), div_zero, zero_mul, add_zero]
