English
For k ≥ 2 and x ∈ [0,1], the HasSum of the series ∑ 1/n^k · fourier(n,x) equals -(2π i)^k/k! · bernoulliFun(k,x).
Русский
Для k ≥ 2 и x ∈ [0,1] имеет место равенство суммирования: ∑_{n≥1} (fourier(n,x))/n^k = -(2π i)^k/k! · bernoulliFun(k,x).
LaTeX
$$$\text{HasSum}\left( \sum_{n \in \mathbb{Z}} \dfrac{1}{n^{k}} \cdot \text{fourier}(n,x) \right) = -\dfrac{(2\pi i)^{k}}{k!} \; \text{bernoulliFun}(k,x).$$$
Lean4
theorem hasSum_one_div_pow_mul_fourier_mul_bernoulliFun {k : ℕ} (hk : 2 ≤ k) {x : ℝ} (hx : x ∈ Icc (0 : ℝ) 1) :
HasSum (fun n : ℤ => 1 / (n : ℂ) ^ k * fourier n (x : 𝕌)) (-(2 * π * I) ^ k / k ! * bernoulliFun k x) := by
-- first show it suffices to prove result for `Ico 0 1`
suffices
∀ {y : ℝ},
y ∈ Ico (0 : ℝ) 1 →
HasSum (fun (n : ℤ) ↦ 1 / (n : ℂ) ^ k * fourier n y) (-(2 * (π : ℂ) * I) ^ k / k ! * bernoulliFun k y)
by
rw [← Ico_insert_right (zero_le_one' ℝ), mem_insert_iff, or_comm] at hx
rcases hx with (hx | rfl)
· exact this hx
· convert this (left_mem_Ico.mpr zero_lt_one) using 1
· rw [AddCircle.coe_period, QuotientAddGroup.mk_zero]
· rw [bernoulliFun_endpoints_eq_of_ne_one (by cutsat : k ≠ 1)]
intro y hy
let B : C(𝕌, ℂ) :=
ContinuousMap.mk ((↑) ∘ periodizedBernoulli k) (continuous_ofReal.comp (periodizedBernoulli.continuous (by cutsat)))
have step1 : ∀ n : ℤ, fourierCoeff B n = -k ! / (2 * π * I * n) ^ k := by rw [ContinuousMap.coe_mk];
exact fourierCoeff_bernoulli_eq (by cutsat : k ≠ 0)
have step2 :=
has_pointwise_sum_fourier_series_of_summable ((summable_bernoulli_fourier hk).congr fun n => (step1 n).symm) y
simp_rw [step1] at step2
convert step2.mul_left (-(2 * ↑π * I) ^ k / (k ! : ℂ)) using 2 with n
· rw [smul_eq_mul, ← mul_assoc, mul_div, mul_neg, div_mul_cancel₀, neg_neg, mul_pow _ (n : ℂ), ← div_div, div_self]
· rw [Ne, pow_eq_zero_iff', not_and_or]
exact Or.inl two_pi_I_ne_zero
· exact Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)
·
rw [ContinuousMap.coe_mk, Function.comp_apply, ofReal_inj, periodizedBernoulli,
AddCircle.liftIco_coe_apply (show y ∈ Ico 0 (0 + 1) by rwa [zero_add])]
