From c521336dfb09896b52bc1bf6b613e978b9a3754c Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 23 Mar 2021 19:49:34 +0000 Subject: [PATCH] feat(data/polynomial/bernstein): identities (#6470) Co-authored-by: Scott Morrison --- src/data/mv_polynomial/pderiv.lean | 46 ++++++++ src/data/polynomial/basic.lean | 8 ++ src/ring_theory/polynomial/bernstein.lean | 132 +++++++++++++++++++++- 3 files changed, 181 insertions(+), 5 deletions(-) diff --git a/src/data/mv_polynomial/pderiv.lean b/src/data/mv_polynomial/pderiv.lean index fa6324264cc94..ba247d5a4d034 100644 --- a/src/data/mv_polynomial/pderiv.lean +++ b/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 diff --git a/src/data/polynomial/basic.lean b/src/data/polynomial/basic.lean index af0b3cd2baeb2..f0e0227368337 100644 --- a/src/data/polynomial/basic.lean +++ b/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 diff --git a/src/ring_theory/polynomial/bernstein.lean b/src/ring_theory/polynomial/bernstein.lean index b93f541245913..f99be9440c881 100644 --- a/src/ring_theory/polynomial/bernstein.lean +++ b/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