English
For the unique nontrivial Dirichlet character modulo 4, the L-value at 3 equals π^3/32: ∑_{n≥1} (1/n^3) sin(π n/2) = π^3/32.
Русский
Для единственного непериодного Дирихле-символа модуль 4 значение L(χ,3) равно π^3/32: сумма синусов даёт π^3/32.
LaTeX
$$$\sum_{n=1}^{\infty} \dfrac{\sin(\pi n/2)}{n^{3}} = \dfrac{\pi^{3}}{32}.$$$
Lean4
/-- Explicit formula for `L(χ, 3)`, where `χ` is the unique nontrivial Dirichlet character modulo 4.
-/
theorem hasSum_L_function_mod_four_eval_three :
HasSum (fun n : ℕ => (1 : ℝ) / (n : ℝ) ^ 3 * Real.sin (π * n / 2)) (π ^ 3 / 32) :=
by
apply (congr_arg₂ HasSum ?_ ?_).to_iff.mp <| hasSum_one_div_nat_pow_mul_sin one_ne_zero (?_ : 1 / 4 ∈ Icc (0 : ℝ) 1)
· ext1 n
norm_num
left
congr 1
ring
· have : (1 / 4 : ℝ) = (algebraMap ℚ ℝ) (1 / 4 : ℚ) := by simp
rw [this, mul_pow, Polynomial.eval_map, Polynomial.eval₂_at_apply, (by decide : 2 * 1 + 1 = 3),
Polynomial.bernoulli_three_eval_one_quarter]
norm_num [Nat.factorial]; field_simp; ring
· rw [mem_Icc]; constructor
· linarith
· linarith
