feat(number_theory/bernoulli): Results regarding Bernoulli numbers as…

… a generating function (#5957)

We prove that the Bernoulli numbers are generating functions for t/(e^t - 1). Most of the results are proved by @kbuzzard.



Co-authored-by: laughinggas <58670661+laughinggas@users.noreply.github.com>

src/algebra/big_operators/nat_antidiagonal.lean

@@ -55,13 +55,20 @@ lemma prod_antidiagonal_subst {n : ℕ} {f : ℕ × ℕ → ℕ → M} :
 prod_congr rfl $ λ p hp, by rw [nat.mem_antidiagonal.1 hp]
 
 @[to_additive]
-lemma prod_antidiagonal_eq_prod_range_succ {M : Type*} [comm_monoid M] (f : ℕ → ℕ → M) (n : ℕ) :
-  ∏ ij in finset.nat.antidiagonal n, f ij.1 ij.2 = ∏ k in range n.succ, f k (n - k) :=
+lemma prod_antidiagonal_eq_prod_range_succ_mk {M : Type*} [comm_monoid M] (f : ℕ × ℕ → M) (n : ℕ) :
+  ∏ ij in finset.nat.antidiagonal n, f ij = ∏ k in range n.succ, f (k, n - k) :=
 begin
   convert prod_map _ ⟨λ i, (i, n - i), λ x y h, (prod.mk.inj h).1⟩ _,
   refl,
 end
 
+/-- This lemma matches more generally than `finset.nat.prod_antidiagonal_eq_prod_range_succ_mk` when
+using `rw ←`. -/
+@[to_additive]
+lemma prod_antidiagonal_eq_prod_range_succ {M : Type*} [comm_monoid M] (f : ℕ → ℕ → M) (n : ℕ) :
+  ∏ ij in finset.nat.antidiagonal n, f ij.1 ij.2 = ∏ k in range n.succ, f k (n - k) :=
+prod_antidiagonal_eq_prod_range_succ_mk _ _
+
 end nat
 
 end finset

src/data/nat/choose/basic.lean

@@ -112,9 +112,19 @@ begin
   exact (nat.div_eq_of_eq_mul_left (mul_pos (factorial_pos _) (factorial_pos _)) this).symm
 end
 
+lemma add_choose (i j : ℕ) : (i + j).choose j = factorial (i + j) / (factorial i * factorial j) :=
+by rw [choose_eq_factorial_div_factorial (le_add_left j i), nat.add_sub_cancel, mul_comm]
+
 theorem factorial_mul_factorial_dvd_factorial {n k : ℕ} (hk : k ≤ n) : k! * (n - k)! ∣ n! :=
 by rw [←choose_mul_factorial_mul_factorial hk, mul_assoc]; exact dvd_mul_left _ _
 
+lemma factorial_mul_factorial_dvd_factorial_add (i j : ℕ) :
+  i! * j! ∣ (i + j)! :=
+begin
+  convert factorial_mul_factorial_dvd_factorial (le.intro rfl),
+  rw nat.add_sub_cancel_left
+end
+
 @[simp] lemma choose_symm {n k : ℕ} (hk : k ≤ n) : choose n (n-k) = choose n k :=
 by rw [choose_eq_factorial_div_factorial hk, choose_eq_factorial_div_factorial (sub_le _ _),
   nat.sub_sub_self hk, mul_comm]

src/number_theory/bernoulli.lean

@@ -5,6 +5,8 @@ Authors: Johan Commelin, Kevin Buzzard
 -/
 import data.rat
 import data.fintype.card
+import algebra.big_operators.nat_antidiagonal
+import ring_theory.power_series.well_known
 
 /-!
 # Bernoulli numbers
@@ -65,6 +67,8 @@ This formula is true for all $n$ and in particular $B_0=1$.
 -/
 
 open_locale big_operators
+open nat
+open finset
 
 /-!
 
@@ -87,6 +91,24 @@ lemma bernoulli_def (n : ℕ) :
   bernoulli n = 1 - ∑ k in finset.range n, (n.choose k) / (n - k + 1) * bernoulli k :=
 by { rw [bernoulli_def', ← fin.sum_univ_eq_sum_range], refl }
 
+lemma bernoulli_spec (n : ℕ) :
+  ∑ k in finset.range n.succ, (n.choose (n - k) : ℚ) / (n - k + 1) * bernoulli k = 1 :=
+begin
+  rw [finset.sum_range_succ, bernoulli_def n, nat.sub_self],
+  conv in (nat.choose _ (_ - _)) { rw choose_symm (le_of_lt (finset.mem_range.1 H)) },
+  simp only [one_mul, cast_one, sub_self, sub_add_cancel, choose_zero_right, zero_add, div_one],
+end
+
+lemma bernoulli_spec' (n : ℕ) :
+  ∑ k in finset.nat.antidiagonal n,
+  ((k.1 + k.2).choose k.2 : ℚ) / (k.2 + 1) * bernoulli k.1 = 1 :=
+begin
+  refine ((nat.sum_antidiagonal_eq_sum_range_succ_mk _ n).trans _).trans (bernoulli_spec n),
+  refine sum_congr rfl (λ x hx, _),
+  rw mem_range_succ_iff at hx,
+  simp [nat.add_sub_cancel' hx, cast_sub hx],
+end
+
 /-!
 
 ### Examples
@@ -139,8 +161,46 @@ begin
   rw ← cast_sub hk,
   congr',
   field_simp [show ((n - k : ℕ) : ℚ) + 1 ≠ 0, by {norm_cast, simp}],
-  -- down to nat
   norm_cast,
   rw [mul_comm, nat.sub_add_eq_add_sub hk],
   exact choose_mul_succ_eq n k,
 end
+
+open power_series
+open nat
+
+theorem bernoulli_power_series :
+  power_series.mk (λ n, (bernoulli n / nat.factorial n : ℚ)) * (exp ℚ - 1) = X * exp ℚ :=
+begin
+  ext n,
+  -- constant coefficient is a special case
+  cases n,
+  { simp only [ring_hom.map_sub, constant_coeff_one, zero_mul, constant_coeff_exp, constant_coeff_X,
+      coeff_zero_eq_constant_coeff, mul_zero, sub_self, ring_hom.map_mul] },
+  rw [coeff_mul, mul_comm X, coeff_succ_mul_X],
+  simp only [coeff_mk, coeff_one, coeff_exp, linear_map.map_sub, factorial,
+    rat.algebra_map_rat_rat, nat.sum_antidiagonal_succ', if_pos],
+  simp only [factorial, prod.snd, one_div, cast_succ, cast_one, cast_mul, ring_hom.id_apply,
+    sub_zero, add_eq_zero_iff, if_false, zero_add, one_ne_zero,
+    factorial, div_one, mul_zero, and_false, sub_self],
+  apply eq_inv_of_mul_left_eq_one,
+  rw sum_mul,
+  convert bernoulli_spec' n using 1,
+  apply sum_congr rfl,
+  rintro ⟨i, j⟩ hn, 
+  rw nat.mem_antidiagonal at hn, 
+  subst hn, 
+  dsimp only,
+  have hj : (j : ℚ) + 1 ≠ 0, by { norm_cast, linarith },
+  have hj' : j.succ ≠ 0, by { show j + 1 ≠ 0, by linarith },
+  have hnz : (j + 1 : ℚ) * nat.factorial j * nat.factorial i ≠ 0,
+  { norm_cast at *,
+    exact mul_ne_zero (mul_ne_zero hj (factorial_ne_zero j)) (factorial_ne_zero _), },
+  field_simp [hj, hnz],
+  rw [mul_comm _ (bernoulli i), mul_assoc],
+  norm_cast,
+  rw [mul_comm (j + 1) _, mul_div_assoc, ← mul_assoc, cast_mul, cast_mul, mul_div_mul_right _,
+    add_choose, cast_dvd_char_zero],
+  { apply factorial_mul_factorial_dvd_factorial_add, },
+  { exact cast_ne_zero.mpr hj', },
+end

src/ring_theory/power_series/well_known.lean

@@ -73,6 +73,8 @@ variables {A A'} (n : ℕ) (f : A →+* A')
 
 @[simp] lemma coeff_exp : coeff A n (exp A) = algebra_map ℚ A (1 / n!) := coeff_mk _ _
 
+@[simp] lemma constant_coeff_exp : constant_coeff A (exp A) = 1 := ring_hom.map_one _
+
 @[simp] lemma map_exp : map (f : A →+* A') (exp A) = exp A' := by { ext, simp }
 
 @[simp] lemma map_sin : map f (sin A) = sin A' := by { ext, simp [sin, apply_ite f] }