feat(data/polynomial): Bernstein polynomials (#6465)

The definition of the Bernstein polynomials
`bernstein_polynomial (R : Type*) [ring R] (n ν : ℕ) : polynomial R := (choose n ν) * X^ν * (1 - X)^(n - ν)`
and the fact that for `ν : fin (n+1)` these are linearly independent over `ℚ`.

(Future work: use these to prove Weierstrass' theorem that polynomials are dense in `C([0,1], ℝ)`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/group_power/basic.lean

@@ -394,12 +394,25 @@ f.to_monoid_hom.map_pow a
 
 end ring_hom
 
+section
+variables (R)
+
 theorem neg_one_pow_eq_or [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
 | 0     := or.inl rfl
 | (n+1) := (neg_one_pow_eq_or n).swap.imp
   (λ h, by rw [pow_succ, h, neg_one_mul, neg_neg])
   (λ h, by rw [pow_succ, h, mul_one])
 
+end
+
+@[simp]
+lemma neg_one_pow_mul_eq_zero_iff [ring R] {n : ℕ} {r : R} : (-1)^n * r = 0 ↔ r = 0 :=
+by rcases neg_one_pow_eq_or R n; simp [h]
+
+@[simp]
+lemma mul_neg_one_pow_eq_zero_iff [ring R] {n : ℕ} {r : R} : r * (-1)^n = 0 ↔ r = 0 :=
+by rcases neg_one_pow_eq_or R n; simp [h]
+
 lemma pow_dvd_pow [monoid R] (a : R) {m n : ℕ} (h : m ≤ n) :
   a ^ m ∣ a ^ n := ⟨a ^ (n - m), by rw [← pow_add, nat.add_comm, nat.sub_add_cancel h]⟩
 

src/data/fin.lean

@@ -1105,6 +1105,9 @@ variables {α : fin (n+1) → Type u} (x : α 0) (q : Πi, α i) (p : Π(i : fin
 /-- The tail of an `n+1` tuple, i.e., its last `n` entries. -/
 def tail (q : Πi, α i) : (Π(i : fin n), α (i.succ)) := λ i, q i.succ
 
+lemma tail_def {n : ℕ} {α : fin (n+1) → Type*} {q : Π i, α i} :
+  tail (λ k : fin (n+1), q k) = (λ k : fin n, q k.succ) := rfl
+
 /-- Adding an element at the beginning of an `n`-tuple, to get an `n+1`-tuple. -/
 def cons (x : α 0) (p : Π(i : fin n), α (i.succ)) : Πi, α i :=
 λ j, fin.cases x p j
@@ -1238,6 +1241,9 @@ variables {α : fin (n+1) → Type u} (x : α (last n)) (q : Πi, α i) (p : Π(
 def init (q : Πi, α i) (i : fin n) : α i.cast_succ :=
 q i.cast_succ
 
+lemma init_def {n : ℕ} {α : fin (n+1) → Type*} {q : Π i, α i} :
+  init (λ k : fin (n+1), q k) = (λ k : fin n, q k.cast_succ) := rfl
+
 /-- Adding an element at the end of an `n`-tuple, to get an `n+1`-tuple. The name `snoc` comes from
 `cons` (i.e., adding an element to the left of a tuple) read in reverse order. -/
 def snoc (p : Π(i : fin n), α i.cast_succ) (x : α (last n)) (i : fin (n+1)) : α i :=

src/data/int/basic.lean

@@ -1071,6 +1071,9 @@ lemma units_inv_eq_self (u : units ℤ) : u⁻¹ = u :=
 @[simp] lemma units_coe_mul_self (u : units ℤ) : (u * u : ℤ) = 1 :=
 by rw [←units.coe_mul, units_mul_self, units.coe_one]
 
+@[simp] lemma neg_one_pow_ne_zero {n : ℕ} : (-1 : ℤ)^n ≠ 0 :=
+pow_ne_zero _ (abs_pos.mp trivial)
+
 /-! ### bitwise ops -/
 
 @[simp] lemma bodd_zero : bodd 0 = ff := rfl

src/data/polynomial/derivative.lean

@@ -286,6 +286,24 @@ end
 
 end comm_semiring
 
+section comm_ring
+variables [comm_ring R]
+
+lemma derivative_comp_one_sub_X (p : polynomial R) :
+  (p.comp (1-X)).derivative = -p.derivative.comp (1-X) :=
+by simp [derivative_comp]
+
+@[simp]
+lemma iterate_derivative_comp_one_sub_X (p : polynomial R) (k : ℕ) :
+  derivative^[k] (p.comp (1-X)) = (-1)^k * (derivative^[k] p).comp (1-X) :=
+begin
+  induction k with k ih generalizing p,
+  { simp, },
+  { simp [ih p.derivative, iterate_derivative_neg, derivative_comp, pow_succ], },
+end
+
+end comm_ring
+
 section domain
 variables [integral_domain R]
 

src/linear_algebra/multilinear.lean

@@ -911,7 +911,7 @@ end
 @[simp] lemma multilinear_map.uncurry_curry_left
   (f : multilinear_map R M M₂) :
   f.curry_left.uncurry_left = f :=
-by { ext m, simp }
+by { ext m, simp, }
 
 variables (R M M₂)
 

src/number_theory/quadratic_reciprocity.lean

@@ -402,7 +402,7 @@ have (legendre_sym a p : zmod p) = (((-1)^((Ico 1 (p / 2).succ).filter
   by rw [legendre_sym_eq_pow, gauss_lemma_aux₂ p ha0]; simp,
 begin
   cases legendre_sym_eq_one_or_neg_one a p ha0;
-  cases @neg_one_pow_eq_or ℤ _  ((Ico 1 (p / 2).succ).filter
+  cases neg_one_pow_eq_or ℤ ((Ico 1 (p / 2).succ).filter
     (λ x : ℕ, p / 2 < (a * x : zmod p).val)).card;
   simp [*, ne_neg_self p one_ne_zero, (ne_neg_self p one_ne_zero).symm] at *
 end