refactor(number_theory/bernoulli_polynomials): improve names (#11805)

Cleanup the bernoulli_polynomials file



Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

src/number_theory/bernoulli_polynomials.lean

@@ -26,14 +26,14 @@ Bernoulli polynomials are defined using `bernoulli`, the Bernoulli numbers.
 
 ## Main theorems
 
-- `sum_bernoulli_poly`: The sum of the $k^\mathrm{th}$ Bernoulli polynomial with binomial
+- `sum_bernoulli`: The sum of the $k^\mathrm{th}$ Bernoulli polynomial with binomial
   coefficients up to n is `(n + 1) * X^n`.
-- `exp_bernoulli_poly`: The Bernoulli polynomials act as generating functions for the exponential.
+- `bernoulli_generating_function`: The Bernoulli polynomials act as generating functions
+  for the exponential.
 
 ## TODO
 
-- `bernoulli_poly_eval_one_neg` : $$ B_n(1 - x) = (-1)^n*B_n(x) $$
-- ``bernoulli_poly_eval_one` : Follows as a consequence of `bernoulli_poly_eval_one_neg`.
+- `bernoulli_eval_one_neg` : $$ B_n(1 - x) = (-1)^n*B_n(x) $$
 
 -/
 
@@ -43,45 +43,45 @@ open_locale nat
 
 open nat finset
 
+namespace polynomial
+
 /-- The Bernoulli polynomials are defined in terms of the negative Bernoulli numbers. -/
-def bernoulli_poly (n : ℕ) : polynomial ℚ :=
-  ∑ i in range (n + 1), polynomial.monomial (n - i) ((bernoulli i) * (choose n i))
+def bernoulli (n : ℕ) : polynomial ℚ :=
+  ∑ i in range (n + 1), polynomial.monomial (n - i) ((_root_.bernoulli i) * (choose n i))
 
-lemma bernoulli_poly_def (n : ℕ) : bernoulli_poly n =
-  ∑ i in range (n + 1), polynomial.monomial i ((bernoulli (n - i)) * (choose n i)) :=
+lemma bernoulli_def (n : ℕ) : bernoulli n =
+  ∑ i in range (n + 1), polynomial.monomial i ((_root_.bernoulli (n - i)) * (choose n i)) :=
 begin
-  rw [←sum_range_reflect, add_succ_sub_one, add_zero, bernoulli_poly],
+  rw [←sum_range_reflect, add_succ_sub_one, add_zero, bernoulli],
   apply sum_congr rfl,
   rintros x hx,
   rw mem_range_succ_iff at hx, rw [choose_symm hx, tsub_tsub_cancel_of_le hx],
 end
 
-namespace bernoulli_poly
-
 /-
 ### examples
 -/
 
 section examples
 
-@[simp] lemma bernoulli_poly_zero : bernoulli_poly 0 = 1 :=
-by simp [bernoulli_poly]
+@[simp] lemma bernoulli_zero : bernoulli 0 = 1 :=
+by simp [bernoulli]
 
-@[simp] lemma bernoulli_poly_eval_zero (n : ℕ) : (bernoulli_poly n).eval 0 = bernoulli n :=
+@[simp] lemma bernoulli_eval_zero (n : ℕ) : (bernoulli n).eval 0 = _root_.bernoulli n :=
 begin
- rw [bernoulli_poly, polynomial.eval_finset_sum, sum_range_succ],
-  have : ∑ (x : ℕ) in range n, bernoulli x * (n.choose x) * 0 ^ (n - x) = 0,
+ rw [bernoulli, polynomial.eval_finset_sum, sum_range_succ],
+  have : ∑ (x : ℕ) in range n, _root_.bernoulli x * (n.choose x) * 0 ^ (n - x) = 0,
   { apply sum_eq_zero (λ x hx, _),
     have h : 0 < n - x := tsub_pos_of_lt (mem_range.1 hx),
     simp [h] },
   simp [this],
 end
 
-@[simp] lemma bernoulli_poly_eval_one (n : ℕ) : (bernoulli_poly n).eval 1 = bernoulli' n :=
+@[simp] lemma bernoulli_eval_one (n : ℕ) : (bernoulli n).eval 1 = _root_.bernoulli' n :=
 begin
-  simp only [bernoulli_poly, polynomial.eval_finset_sum],
+  simp only [bernoulli, 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,
+    (_root_.bernoulli _).mul_comm, sum_bernoulli, one_pow, mul_one, polynomial.eval_C,
     polynomial.eval_monomial],
   by_cases h : n = 1,
   { norm_num [h], },
@@ -91,14 +91,14 @@ end
 
 end examples
 
-@[simp] theorem sum_bernoulli_poly (n : ℕ) :
-  ∑ k in range (n + 1), ((n + 1).choose k : ℚ) • bernoulli_poly k =
+@[simp] theorem sum_bernoulli (n : ℕ) :
+  ∑ k in range (n + 1), ((n + 1).choose k : ℚ) • bernoulli k =
     polynomial.monomial n (n + 1 : ℚ) :=
 begin
- simp_rw [bernoulli_poly_def, finset.smul_sum, finset.range_eq_Ico, ←finset.sum_Ico_Ico_comm,
+ simp_rw [bernoulli_def, finset.smul_sum, finset.range_eq_Ico, ←finset.sum_Ico_Ico_comm,
     finset.sum_Ico_eq_sum_range],
   simp only [cast_succ, add_tsub_cancel_left, tsub_zero, zero_add, linear_map.map_add],
-  simp_rw [polynomial.smul_monomial, mul_comm (bernoulli _) _, smul_eq_mul, ←mul_assoc],
+  simp_rw [polynomial.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 H).1
@@ -107,7 +107,7 @@ begin
     rw [←sum_smul], },
   rw [sum_range_succ_comm],
   simp only [add_right_eq_self, cast_succ, mul_one, cast_one, cast_add, add_tsub_cancel_left,
-    choose_succ_self_right, one_smul, bernoulli_zero, sum_singleton, zero_add,
+    choose_succ_self_right, one_smul, _root_.bernoulli_zero, sum_singleton, zero_add,
     linear_map.map_add, range_one],
   apply sum_eq_zero (λ x hx, _),
   have f : ∀ x ∈ range n, ¬ n + 1 - x = 1,
@@ -123,23 +123,23 @@ begin
 end
 
 open power_series
-open polynomial (aeval)
 variables {A : Type*} [comm_ring A] [algebra ℚ A]
 
 -- TODO: define exponential generating functions, and use them here
 -- This name should probably be updated afterwards
 
 /-- The theorem that `∑ Bₙ(t)X^n/n!)(e^X-1)=Xe^{tX}`  -/
-theorem exp_bernoulli_poly' (t : A) :
-  mk (λ n, aeval t ((1 / n! : ℚ) • bernoulli_poly n)) * (exp A - 1) = X * rescale t (exp A) :=
+theorem bernoulli_generating_function (t : A) :
+  mk (λ n, aeval t ((1 / n! : ℚ) • bernoulli n)) * (exp A - 1) =
+    power_series.X * rescale t (exp A) :=
 begin
   -- check equality of power series by checking coefficients of X^n
   ext n,
   -- n = 0 case solved by `simp`
   cases n, { simp },
   -- n ≥ 1, the coefficients is a sum to n+2, so use `sum_range_succ` to write as
   -- last term plus sum to n+1
-  rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, coeff_mul,
+  rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, power_series.coeff_mul,
     nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ],
   -- last term is zero so kill with `add_zero`
   simp only [ring_hom.map_sub, tsub_self, constant_coeff_one, constant_coeff_exp,
@@ -158,21 +158,21 @@ begin
     (show (n! : ℚ) ≠ 0, from cast_ne_zero.2 (factorial_ne_zero n)), mul_one, mul_comm (t^n),
     ← polynomial.aeval_monomial, cast_add, cast_one],
   -- But this is the RHS of `sum_bernoulli_poly`
-  rw [← sum_bernoulli_poly, finset.mul_sum, alg_hom.map_sum],
+  rw [← sum_bernoulli, finset.mul_sum, alg_hom.map_sum],
   -- and now we have to prove a sum is a sum, but all the terms are equal.
   apply finset.sum_congr rfl,
   -- The rest is just trivialities, hampered by the fact that we're coercing
   -- factorials and binomial coefficients between ℕ and ℚ and A.
   intros i hi,
   -- deal with coefficients of e^X-1
   simp only [nat.cast_choose ℚ (mem_range_le hi), coeff_mk,
-    if_neg (mem_range_sub_ne_zero hi), one_div, alg_hom.map_smul, coeff_one, units.coe_mk,
-    coeff_exp, sub_zero, linear_map.map_sub, algebra.smul_mul_assoc, algebra.smul_def,
+    if_neg (mem_range_sub_ne_zero hi), one_div, alg_hom.map_smul, power_series.coeff_one,
+    units.coe_mk, coeff_exp, sub_zero, linear_map.map_sub, algebra.smul_mul_assoc, algebra.smul_def,
     mul_right_comm _ ((aeval t) _), ←mul_assoc, ← ring_hom.map_mul, succ_eq_add_one],
   -- finally cancel the Bernoulli polynomial and the algebra_map
   congr',
   apply congr_arg,
   rw [mul_assoc, div_eq_mul_inv, ← mul_inv₀],
 end
 
-end bernoulli_poly
+end polynomial