feat(data/polynomial/bernstein): identities (#6470)

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

src/data/mv_polynomial/pderiv.lean

@@ -74,11 +74,15 @@ lemma pderiv_monomial {i : σ} :
   pderiv i (monomial s a) = monomial (s - single i 1) (a * (s i)) :=
 by simp only [pderiv, monomial_zero, sum_monomial, zero_mul, linear_map.coe_mk]
 
+
 @[simp]
 lemma pderiv_C {i : σ} : pderiv i (C a) = 0 :=
 suffices pderiv i (monomial 0 a) = 0, by simpa,
 by simp only [monomial_zero, pderiv_monomial, nat.cast_zero, mul_zero, zero_apply]
 
+@[simp]
+lemma pderiv_one {i : σ} : pderiv i (1 : mv_polynomial σ R) = 0 := pderiv_C
+
 lemma pderiv_eq_zero_of_not_mem_vars {i : σ} {f : mv_polynomial σ R} (h : i ∉ f.vars) :
   pderiv i f = 0 :=
 begin
@@ -89,6 +93,25 @@ begin
   simp [mem_support_not_mem_vars_zero H h],
 end
 
+lemma pderiv_X {i j : σ} : pderiv i (X j : mv_polynomial σ R) = if i = j then 1 else 0 :=
+begin
+  dsimp [pderiv],
+  erw finsupp.sum_single_index,
+  simp only [mul_boole, if_congr, finsupp.single_apply, nat.cast_zero, nat.cast_one, nat.cast_ite],
+  by_cases h : i = j,
+  { rw [if_pos h, if_pos h.symm],
+    subst h,
+    congr,
+    ext j,
+    simp, },
+  { rw [if_neg h, if_neg (ne.symm h)],
+    simp, },
+  { simp, },
+end
+
+@[simp] lemma pderiv_X_self {i : σ} : pderiv i (X i : mv_polynomial σ R) = 1 :=
+by simp [pderiv_X]
+
 lemma pderiv_monomial_single {i : σ} {n : ℕ} :
   pderiv i (monomial (single i n) a) = monomial (single i (n-1)) (a * n) :=
 by simp
@@ -132,6 +155,29 @@ lemma pderiv_C_mul {f : mv_polynomial σ R} {i : σ} :
   pderiv i (C a * f) = C a * pderiv i f :=
 by convert linear_map.map_smul (pderiv i) a f; rw C_mul'
 
+@[simp]
+lemma pderiv_pow {i : σ} {f : mv_polynomial σ R} {n : ℕ} :
+  pderiv i (f^n) = n * pderiv i f * f^(n-1) :=
+begin
+  induction n with n ih,
+  { simp, },
+  { simp only [nat.succ_sub_succ_eq_sub, nat.cast_succ, nat.sub_zero, mv_polynomial.pderiv_mul,
+      pow_succ, ih],
+    cases n,
+    { simp, },
+    { simp only [nat.succ_eq_add_one, nat.add_succ_sub_one, add_zero, nat.cast_add, nat.cast_one,
+        pow_succ],
+      ring, }, },
+end
+
+@[simp]
+lemma pderiv_nat_cast {i : σ} {n : ℕ} : pderiv i (n : mv_polynomial σ R) = 0 :=
+begin
+  induction n with n ih,
+  { simp, },
+  { simp [ih], },
+end
+
 end pderiv
 
 end mv_polynomial

src/data/polynomial/basic.lean

@@ -228,6 +228,14 @@ lemma monomial_left_inj {R : Type*} [semiring R] {a : R} (ha : a ≠ 0) {i j : 
   (monomial i a) = (monomial j a) ↔ i = j :=
 finsupp.single_left_inj ha
 
+lemma nat_cast_mul {R : Type*} [semiring R] (n : ℕ) (p : polynomial R) :
+  (n : polynomial R) * p = n • p :=
+begin
+  induction n with n ih,
+  { simp, },
+  { simp [ih, nat.succ_eq_add_one, add_smul, add_mul], },
+end
+
 end semiring
 
 section comm_semiring

src/ring_theory/polynomial/bernstein.lean

@@ -5,6 +5,8 @@ Authors: Scott Morrison
 -/
 import data.polynomial.derivative
 import data.polynomial.algebra_map
+import data.mv_polynomial.pderiv
+import data.nat.choose.sum
 import linear_algebra.basis
 import ring_theory.polynomial.pochhammer
 import tactic.omega
@@ -19,15 +21,16 @@ bernstein_polynomial (R : Type*) [comm_ring R] (n ν : ℕ) : polynomial R :=
 ```
 and the fact that for `ν : fin (n+1)` these are linearly independent over `ℚ`.
 
-## Future work
-
-The basic identities
+We prove the basic identities
 * `(finset.range (n + 1)).sum (λ ν, bernstein_polynomial R n ν) = 1`
 * `(finset.range (n + 1)).sum (λ ν, ν • bernstein_polynomial R n ν) = n • X`
 * `(finset.range (n + 1)).sum (λ ν, (ν * (ν-1)) • bernstein_polynomial R n ν) = (n * (n-1)) • X^2`
-and the fact that the Bernstein approximations
+
+## Future work
+
+The fact that the Bernstein approximations
 of a continuous function `f` on `[0,1]` converge uniformly.
-This will give a constructive proof of Weierstrass's theorem that
+This will give a constructive proof of Weierstrass' theorem that
 polynomials are dense in `C([0,1], ℝ)`.
 -/
 
@@ -331,4 +334,123 @@ lemma linear_independent (n : ℕ) :
   linear_independent ℚ (λ ν : fin (n+1), bernstein_polynomial ℚ n ν) :=
 linear_independent_aux n (n+1) (le_refl _)
 
+lemma sum (n : ℕ) : (finset.range (n + 1)).sum (λ ν, bernstein_polynomial R n ν) = 1 :=
+begin
+  -- We calculate `(x + (1-x))^n` in two different ways.
+  conv { congr, congr, skip, funext, dsimp [bernstein_polynomial], rw [mul_assoc, mul_comm], },
+  rw ←add_pow,
+  simp,
+end
+
+
+open polynomial
+open mv_polynomial
+
+lemma sum_smul (n : ℕ) :
+  (finset.range (n + 1)).sum (λ ν, ν • bernstein_polynomial R n ν) = n • X :=
+begin
+  -- We calculate the `x`-derivative of `(x+y)^n`, evaluated at `y=(1-x)`,
+  -- either directly or by using the binomial theorem.
+
+  -- We'll work in `mv_polynomial bool R`.
+  let x : mv_polynomial bool R := mv_polynomial.X tt,
+  let y : mv_polynomial bool R := mv_polynomial.X ff,
+
+  have pderiv_tt_x : pderiv tt x = 1, { simp [x], },
+  have pderiv_tt_y : pderiv tt y = 0, { simp [pderiv_X, y], },
+
+  let e : bool → polynomial R := λ i, cond i X (1-X),
+
+  -- Start with `(x+y)^n = (x+y)^n`,
+  -- take the `x`-derivative, evaluate at `x=X, y=1-X`, and multiply by `X`:
+  have h : (x+y)^n = (x+y)^n := rfl,
+  apply_fun (pderiv tt) at h,
+  apply_fun (aeval e) at h,
+  apply_fun (λ p, p * X) at h,
+
+  -- On the left hand side we'll use the binomial theorem, then simplify.
+
+  -- We first prepare a tedious rewrite:
+  have w : ∀ k : ℕ,
+    ↑k * polynomial.X ^ (k - 1) * (1 - polynomial.X) ^ (n - k) * ↑(n.choose k) * polynomial.X =
+      k • bernstein_polynomial R n k,
+  { rintro (_|k),
+    { simp, },
+    { dsimp [bernstein_polynomial],
+      simp only [←nat_cast_mul, nat.succ_eq_add_one, nat.add_succ_sub_one, add_zero, pow_succ],
+      push_cast,
+      ring, }, },
+
+  conv at h {
+    to_lhs,
+    rw [add_pow, (pderiv tt).map_sum, (mv_polynomial.aeval e).map_sum, finset.sum_mul],
+    -- Step inside the sum:
+    apply_congr, skip,
+    simp [pderiv_mul, pderiv_tt_x, pderiv_tt_y, e, w], },
+  -- On the right hand side, we'll just simplify.
+  conv at h {
+    to_rhs,
+    rw [pderiv_pow, (pderiv tt).map_add, pderiv_tt_x, pderiv_tt_y],
+    simp [e, nat_cast_mul], },
+  exact h,
+end
+
+lemma sum_mul_smul (n : ℕ) :
+  (finset.range (n + 1)).sum (λ ν, (ν * (ν-1)) • bernstein_polynomial R n ν) =
+    (n * (n-1)) • X^2 :=
+begin
+  -- We calculate the second `x`-derivative of `(x+y)^n`, evaluated at `y=(1-x)`,
+  -- either directly or by using the binomial theorem.
+
+  -- We'll work in `mv_polynomial bool R`.
+  let x : mv_polynomial bool R := mv_polynomial.X tt,
+  let y : mv_polynomial bool R := mv_polynomial.X ff,
+
+  have pderiv_tt_x : pderiv tt x = 1, { simp [x], },
+  have pderiv_tt_y : pderiv tt y = 0, { simp [pderiv_X, y], },
+
+  let e : bool → polynomial R := λ i, cond i X (1-X),
+
+  -- Start with `(x+y)^n = (x+y)^n`,
+  -- take the second `x`-derivative, evaluate at `x=X, y=1-X`, and multiply by `X`:
+  have h : (x+y)^n = (x+y)^n := rfl,
+  apply_fun (pderiv tt) at h,
+  apply_fun (pderiv tt) at h,
+  apply_fun (aeval e) at h,
+  apply_fun (λ p, p * X^2) at h,
+
+  -- On the left hand side we'll use the binomial theorem, then simplify.
+
+  -- We first prepare a tedious rewrite:
+  have w : ∀ k : ℕ,
+    ↑k * (↑(k-1) * polynomial.X ^ (k - 1 - 1)) *
+      (1 - polynomial.X) ^ (n - k) * ↑(n.choose k) * polynomial.X^2 =
+      (k * (k-1)) • bernstein_polynomial R n k,
+  { rintro (_|k),
+    { simp, },
+    { rcases k with (_|k),
+      { simp, },
+      { dsimp [bernstein_polynomial],
+        simp only [←nat_cast_mul, nat.succ_eq_add_one, nat.add_succ_sub_one, add_zero, pow_succ],
+        push_cast,
+        ring, }, }, },
+
+  conv at h {
+    to_lhs,
+    rw [add_pow, (pderiv tt).map_sum, (pderiv tt).map_sum, (mv_polynomial.aeval e).map_sum,
+      finset.sum_mul],
+    -- Step inside the sum:
+    apply_congr, skip,
+    simp [pderiv_mul, pderiv_tt_x, pderiv_tt_y, e, w],
+  },
+  -- On the right hand side, we'll just simplify.
+  conv at h {
+    to_rhs,
+    simp only [pderiv_one, pderiv_mul, pderiv_pow, pderiv_nat_cast, (pderiv tt).map_add,
+      pderiv_tt_x, pderiv_tt_y],
+    simp [e, nat_cast_mul, smul_smul],
+  },
+  exact h,
+end
+
 end bernstein_polynomial