English
A nonrecursive formulation of the sum identity for Bernoulli polynomials: the same Faulhaber-type relation with binomial weights holds for all n.
Русский
Нерекурсивная формулировка тождества суммы Бернулли-полиномов: та же формула Фаульхера с биномиальными весами.
LaTeX
$$sum_bernoulli(n) = ... (nonrec form identical to the recursive version)$$
Lean4
@[simp]
nonrec theorem sum_bernoulli (n : ℕ) :
(∑ k ∈ range (n + 1), ((n + 1).choose k : ℚ) • bernoulli k) = monomial n (n + 1 : ℚ) :=
by
simp_rw [bernoulli_def, Finset.smul_sum, Finset.range_eq_Ico, ← Finset.sum_Ico_Ico_comm, Finset.sum_Ico_eq_sum_range]
simp only [add_tsub_cancel_left, tsub_zero, zero_add, map_add]
simp_rw [smul_monomial, mul_comm (_root_.bernoulli _) _, smul_eq_mul, ← mul_assoc]
conv_lhs =>
apply_congr
· skip
·
conv =>
apply_congr
· skip
·
rw [← Nat.cast_mul,
choose_mul ((le_tsub_iff_left <| mem_range_le (by assumption)).1 <| mem_range_le (by assumption))
(le.intro rfl),
Nat.cast_mul, add_tsub_cancel_left, mul_assoc, mul_comm, ← smul_eq_mul, ← smul_monomial]
simp_rw [← sum_smul]
rw [sum_range_succ_comm]
simp only [add_eq_left, mul_one, cast_one, cast_add, add_tsub_cancel_left, choose_succ_self_right, one_smul,
_root_.bernoulli_zero, sum_singleton, zero_add, map_add, range_one, mul_one]
apply sum_eq_zero fun x hx => _
have f : ∀ x ∈ range n, ¬n + 1 - x = 1 := by grind
intro x hx
rw [sum_bernoulli]
have g : ite (n + 1 - x = 1) (1 : ℚ) 0 = 0 :=
by
simp only [ite_eq_right_iff, one_ne_zero]
intro h₁
exact (f x hx) h₁
rw [g, zero_smul]
