feat(number_theory/bernoulli): bernoulli_power_series (#6456)

Co-authored-by Ashvni Narayanan



Co-authored-by: Moritz Firsching <firsching@google.com>
Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
Co-authored-by: Benjamin Davidson <68528197+benjamindavidson@users.noreply.github.com>

src/data/finset/nat_antidiagonal.lean

@@ -58,6 +58,15 @@ begin
     simp }
 end
 
+/-- A point in the antidiagonal is determined by its first co-ordinate. -/
+lemma antidiagonal_congr {n : ℕ} {p q : ℕ × ℕ} (hp : p ∈ antidiagonal n)
+  (hq : q ∈ antidiagonal n) : p = q ↔ p.fst = q.fst :=
+begin
+  refine ⟨congr_arg prod.fst, (λ h, prod.ext h ((add_right_inj q.fst).mp _))⟩,
+  rw mem_antidiagonal at hp hq,
+  rw [hq, ← h, hp],
+end
+
 end nat
 
 end finset

src/number_theory/bernoulli.lean

@@ -153,21 +153,30 @@ begin
 end
 
 open power_series
+variables (A : Type*) [comm_ring A] [algebra ℚ A]
 
-theorem bernoulli'_power_series :
-  power_series.mk (λ n, (bernoulli' n / n! : ℚ)) * (exp ℚ - 1) = X * exp ℚ :=
+
+/-- The exponential generating function for the Bernoulli numbers `bernoulli' n`. -/
+def bernoulli'_power_series := power_series.mk (λ n, algebra_map ℚ A (bernoulli' n / n!))
+
+theorem bernoulli'_power_series_mul_exp_sub_one :
+  bernoulli'_power_series A * (exp A - 1) = X * exp A :=
 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],
+  rw [bernoulli'_power_series, 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],
+  suffices : ∑ (p : ℕ × ℕ) in nat.antidiagonal n, (bernoulli' p.fst / ↑(p.fst)!)
+                * ((↑(p.snd) + 1) * ↑(p.snd)!)⁻¹ = (↑n!)⁻¹,
+  { convert congr_arg (algebra_map ℚ A) this,
+    simp [ring_hom.map_sum] },
   apply eq_inv_of_mul_left_eq_one,
   rw sum_mul,
   convert bernoulli'_spec' n using 1,
@@ -195,7 +204,8 @@ open ring_hom
 /-- Odd Bernoulli numbers (greater than 1) are zero. -/
 theorem bernoulli'_odd_eq_zero {n : ℕ} (h_odd : odd n) (hlt : 1 < n) : bernoulli' n = 0 :=
 begin
-  have f := bernoulli'_power_series,
+  have f : power_series.mk (λ n, (bernoulli' n / n!)) * (exp ℚ - 1) = X * exp ℚ,
+  { simpa [bernoulli'_power_series] using bernoulli'_power_series_mul_exp_sub_one ℚ },
   have g : eval_neg_hom (mk (λ (n : ℕ), bernoulli' n / ↑(n!)) * (exp ℚ - 1)) * (exp ℚ) =
     (eval_neg_hom (X * exp ℚ)) * (exp ℚ) := by congr',
   rw [map_mul, map_sub, map_one, map_mul, mul_assoc, sub_mul, mul_assoc (eval_neg_hom X) _ _,
@@ -226,6 +236,9 @@ end
 /-- The Bernoulli numbers are defined to be `bernoulli'` with a parity sign. -/
 def bernoulli (n : ℕ) : ℚ := (-1)^n * (bernoulli' n)
 
+lemma bernoulli'_eq_bernoulli (n : ℕ) : bernoulli' n = (-1)^n * bernoulli n :=
+by simp [bernoulli, ← mul_assoc, ← pow_two, ← pow_mul, mul_comm n 2, pow_mul]
+
 @[simp] lemma bernoulli_zero  : bernoulli 0 = 1 := rfl
 
 @[simp] lemma bernoulli_one   : bernoulli 1 = -1/2 :=
@@ -259,3 +272,59 @@ begin
   { ext x, rw bernoulli_eq_bernoulli'_of_ne_one (succ_ne_zero x ∘ succ.inj) },
   { ring },
 end
+
+lemma bernoulli_spec' (n: ℕ) :
+  ∑ k in nat.antidiagonal n,
+  ((k.1 + k.2).choose k.2 : ℚ) / (k.2 + 1) * bernoulli k.1 = if n = 0 then 1 else 0 :=
+begin
+  cases n, { simp },
+  rw if_neg (succ_ne_zero _),
+  -- algebra facts
+  have h₁ : (1, n) ∈ nat.antidiagonal n.succ := by simp [nat.mem_antidiagonal, add_comm],
+  have h₂ : (n:ℚ) + 1 ≠ 0 := by exact_mod_cast succ_ne_zero _,
+  have h₃ : (1 + n).choose n = n + 1 := by simp [add_comm],
+  -- key equation: the corresponding fact for `bernoulli'`
+  have H := bernoulli'_spec' n.succ,
+  -- massage it to match the structure of the goal, then convert piece by piece
+  rw ← add_sum_diff_singleton h₁ at H ⊢,
+  apply add_eq_of_eq_sub',
+  convert eq_sub_of_add_eq' H using 1,
+  { apply sum_congr rfl,
+    intros p h,
+    obtain ⟨h', h''⟩ : p ∈ _ ∧ p ≠ _ := by rwa [mem_sdiff, mem_singleton] at h,
+    have : p.fst ≠ (1, n).fst := by simpa [h''] using nat.antidiagonal_congr h' h₁,
+    simp [this, bernoulli_eq_bernoulli'_of_ne_one] },
+  { field_simp [h₃],
+    norm_num },
+end
+
+/-- The exponential generating function for the Bernoulli numbers `bernoulli n`. -/
+def bernoulli_power_series := power_series.mk (λ n, algebra_map ℚ A (bernoulli n / n!))
+
+theorem bernoulli_power_series_mul_exp_sub_one :
+  bernoulli_power_series A * (exp A - 1) = X :=
+begin
+  ext n,
+  -- constant coefficient is a special case
+  cases n, { simp },
+  simp only [bernoulli_power_series, coeff_mul, coeff_X, nat.sum_antidiagonal_succ', one_div,
+    coeff_mk, coeff_one, coeff_exp, linear_map.map_sub, factorial, if_pos, cast_succ, cast_one,
+    cast_mul, sub_zero, map_one, add_eq_zero_iff, if_false, inv_one, zero_add, one_ne_zero,
+    mul_zero, and_false, sub_self, ←map_mul, ←map_sum],
+  suffices : ∑ x in nat.antidiagonal n, bernoulli x.fst / ↑x.fst! * ((↑x.snd + 1) * ↑x.snd!)⁻¹
+           = if n.succ = 1 then 1 else 0, { split_ifs; simp [h, this] },
+  cases n, { simp },
+  have hfact : ∀ m, (m! : ℚ) ≠ 0 := λ m, by exact_mod_cast factorial_ne_zero m,
+  have hn : n.succ.succ ≠ 1, by { show n + 2 ≠ 1, by linarith },
+  have hite1 : ite (n.succ.succ = 1) 1 0 = (0 / n.succ! : ℚ) := by simp [hn],
+  have hite2 : ite (n.succ = 0) 1 0 = (0 : ℚ) := by simp [succ_ne_zero],
+  rw [hite1, eq_div_iff (hfact n.succ), ←hite2, ←bernoulli_spec', sum_mul],
+  apply sum_congr rfl,
+  rintro ⟨i, j⟩ h,
+  rw nat.mem_antidiagonal at h,
+  have hj : (j.succ : ℚ) ≠ 0 := by exact_mod_cast succ_ne_zero j,
+  field_simp [←h, mul_ne_zero hj (hfact j), hfact i, mul_comm _ (bernoulli i), mul_assoc],
+  rw_mod_cast [mul_comm (j + 1), mul_div_assoc, ← mul_assoc],
+  rw [cast_mul, cast_mul, mul_div_mul_right _ _ hj, add_choose, cast_dvd_char_zero],
+  exact factorial_mul_factorial_dvd_factorial_add i j,
+end