feat(number_theory/bernoulli): bernoulli_poly_eval_one (#6581)

Co-authored-by: Moritz Firsching <firsching@google.com>

src/number_theory/bernoulli.lean

@@ -231,7 +231,7 @@ def bernoulli (n : ℕ) : ℚ := (-1)^n * (bernoulli' n)
 @[simp] lemma bernoulli_one   : bernoulli 1 = -1/2 :=
 by norm_num [bernoulli, bernoulli'_one]
 
-theorem bernoulli_eq_bernoulli' {n : ℕ} (hn : n ≠ 1) : bernoulli n = bernoulli' n :=
+theorem bernoulli_eq_bernoulli'_of_ne_one {n : ℕ} (hn : n ≠ 1) : bernoulli n = bernoulli' n :=
 begin
   by_cases n = 0,
   { rw [h, bernoulli'_zero, bernoulli_zero] },
@@ -242,11 +242,12 @@ begin
     rw mod_two_ne_one at k, simp [k] }
 end
 
-@[simp] theorem sum_bernoulli (n : ℕ) ( h : 2 ≤ n ) :
-  ∑ k in range n, (n.choose k : ℚ) * bernoulli k = 0 :=
+@[simp] theorem sum_bernoulli (n : ℕ):
+  ∑ k in range n, (n.choose k : ℚ) * bernoulli k = if n = 1 then 1 else 0 :=
 begin
-  cases n, norm_num at h,
-  cases n, norm_num at h,
+  cases n, { simp only [sum_empty, range_zero, if_false, zero_ne_one], },
+  cases n, { simp only [mul_one, cast_one, if_true, choose_succ_self_right, eq_self_iff_true,
+    bernoulli_zero, sum_singleton, range_one], },
   rw [sum_range_succ', bernoulli_zero, mul_one, choose_zero_right, cast_one,
     sum_range_succ', bernoulli_one, choose_one_right],
   suffices : ∑ (i : ℕ) in range n, ↑((n + 2).choose (i + 2)) * bernoulli (i + 2) = n/2,
@@ -255,6 +256,6 @@ begin
   simp only [sum_range_succ', one_div, bernoulli'_one, cast_succ, mul_one, cast_one, add_left_inj,
     choose_zero_right, bernoulli'_zero, zero_add, choose_one_right, ← eq_sub_iff_add_eq] at f,
   convert f,
-  { ext x, rw bernoulli_eq_bernoulli' (succ_ne_zero x ∘ succ.inj) },
+  { ext x, rw bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj) },
   { ring },
 end

src/number_theory/bernoulli_polynomials.lean

@@ -76,6 +76,18 @@ begin
   simp [this],
 end
 
+@[simp] lemma bernoulli_poly_eval_one (n : ℕ) : (bernoulli_poly n).eval 1 = bernoulli' n :=
+begin
+  simp only [bernoulli_poly, polynomial.eval_finset_sum],
+  simp only [←succ_eq_add_one, sum_range_succ, mul_one, cast_one, choose_self,
+    (bernoulli _).mul_comm, sum_bernoulli, one_pow, mul_one, polynomial.eval_C,
+    polynomial.eval_monomial],
+  by_cases h : n = 1,
+  { norm_num [h], },
+  { simp [h],
+    exact bernoulli_eq_bernoulli'_of_ne_one h, }
+end
+
 end examples
 
 @[simp] theorem sum_bernoulli_poly (n : ℕ) :
@@ -96,11 +108,18 @@ begin
   simp only [add_right_eq_self, cast_succ, mul_one, cast_one, cast_add, nat.add_sub_cancel_left,
     choose_succ_self_right, one_smul, bernoulli_zero, sum_singleton, zero_add,
     linear_map.map_add, range_one],
-  have f : ∀ x ∈ range n, 2 ≤ n + 1 - x,
-  { rintros x H, rw [mem_range] at H,
-    exact nat.le_sub_left_of_add_le (succ_le_succ H) },
   apply sum_eq_zero (λ x hx, _),
-  rw [sum_bernoulli _ (f x hx), zero_smul],
+  have f : ∀ x ∈ range n, ¬ n + 1 - x = 1,
+  { rintros x H, rw [mem_range] at H,
+    rw [eq_comm],
+    exact ne_of_lt (nat.lt_of_lt_of_le one_lt_two (nat.le_sub_left_of_add_le (succ_le_succ H))),
+  },
+  rw [sum_bernoulli],
+  have g : (ite (n + 1 - x = 1) (1 : ℚ) 0) = 0,
+    { simp only [ite_eq_right_iff, one_ne_zero],
+      intro h₁,
+      exact (f x hx) h₁, },
+  rw [g, zero_smul],
 end
 
 open power_series