feat(data/polynomial/taylor): taylor's formula (#11139)

Via proofs about `hasse_deriv`.
Added some monomial API too.



Co-authored-by: Yakov Pechersky <pechersky@users.noreply.github.com>
Co-authored-by: Yakov Pechersky <ypechersky@treeline.bio>
Co-authored-by: adomani <adomani@gmail.com>
Co-authored-by: damiano <adomani@gmail.com>

src/data/finset/lattice.lean

@@ -86,6 +86,11 @@ begin
   { exact sup_const hs _ }
 end
 
+lemma sup_ite (p : β → Prop) [decidable_pred p] :
+  s.sup (λ i, ite (p i) (f i) (g i)) =
+    (s.filter p).sup f ⊔ (s.filter (λ i, ¬ p i)).sup g :=
+fold_ite _
+
 lemma sup_le {a : α} : (∀b ∈ s, f b ≤ a) → s.sup f ≤ a :=
 sup_le_iff.2
 

src/data/nat/with_bot.lean

@@ -46,4 +46,7 @@ begin
   { exact with_bot.coe_le_coe.mpr (nat.succ_le_iff.mpr (with_bot.coe_lt_coe.mp h)) }
 end
 
+lemma with_bot.lt_one_iff_le_zero {x : with_bot ℕ} : x < 1 ↔ x ≤ 0 :=
+not_iff_not.mp (by simpa using with_bot.one_le_iff_zero_lt)
+
 end nat

src/data/polynomial/degree/definitions.lean

@@ -163,6 +163,9 @@ by { rw [degree, ← monomial_zero_left, support_monomial 0 _ ha, sup_singleton]
 lemma degree_C_le : degree (C a) ≤ 0 :=
 by by_cases h : a = 0; [rw [h, C_0], rw [degree_C h]]; [exact bot_le, exact le_refl _]
 
+lemma degree_C_lt (a : R) : degree (C a) < 1 :=
+nat.with_bot.lt_one_iff_le_zero.mpr degree_C_le
+
 lemma degree_one_le : degree (1 : polynomial R) ≤ (0 : with_bot ℕ) :=
 by rw [← C_1]; exact degree_C_le
 
@@ -999,6 +1002,10 @@ end
   (X ^ n + 1 : polynomial R).leading_coeff = 1 :=
 leading_coeff_X_pow_add_C hn
 
+@[simp] lemma leading_coeff_pow_X_add_C (r : R) (i : ℕ) :
+  leading_coeff ((X + C r) ^ i) = 1 :=
+by { nontriviality, rw leading_coeff_pow'; simp }
+
 end semiring
 
 variables [ring R]

src/data/polynomial/hasse_deriv.lean

@@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 
+import algebra.polynomial.big_operators
 import data.nat.choose.cast
 import data.nat.choose.vandermonde
+import data.polynomial.degree.lemmas
 import data.polynomial.derivative
 
 /-!
@@ -76,6 +78,14 @@ by simp only [hasse_deriv_apply, tsub_zero, nat.choose_zero_right,
 @[simp] lemma hasse_deriv_zero : @hasse_deriv R _ 0 = linear_map.id :=
 linear_map.ext $ hasse_deriv_zero'
 
+lemma hasse_deriv_eq_zero_of_lt_nat_degree (p : polynomial R) (n : ℕ)
+  (h : p.nat_degree < n) : hasse_deriv n p = 0 :=
+begin
+  rw [hasse_deriv_apply, sum_def],
+  refine finset.sum_eq_zero (λ x hx, _),
+  simp [nat.choose_eq_zero_of_lt ((le_nat_degree_of_mem_supp _ hx).trans_lt h)]
+end
+
 lemma hasse_deriv_one' : hasse_deriv 1 f = derivative f :=
 by simp only [hasse_deriv_apply, derivative_apply, monomial_eq_C_mul_X, nat.choose_one_right,
     (nat.cast_commute _ _).eq]
@@ -162,6 +172,40 @@ begin
   all_goals { apply_rules [mul_ne_zero, H] }
 end
 
+lemma nat_degree_hasse_deriv_le (p : polynomial R) (n : ℕ) :
+  nat_degree (hasse_deriv n p) ≤ nat_degree p - n :=
+begin
+  classical,
+  rw [hasse_deriv_apply, sum_def],
+  refine (nat_degree_sum_le _ _).trans _,
+  simp_rw [function.comp, nat_degree_monomial],
+  rw [finset.fold_ite, finset.fold_const],
+  { simp only [if_t_t, max_eq_right, zero_le', finset.fold_max_le, true_and, and_imp,
+               tsub_le_iff_right, mem_support_iff, ne.def, finset.mem_filter],
+    intros x hx hx',
+    have hxp : x ≤ p.nat_degree := le_nat_degree_of_ne_zero hx,
+    have hxn : n ≤ x,
+    { contrapose! hx',
+      simp [nat.choose_eq_zero_of_lt hx'] },
+    rwa [tsub_add_cancel_of_le (hxn.trans hxp)] },
+  { simp }
+end
+
+lemma nat_degree_hasse_deriv [no_zero_smul_divisors ℕ R] (p : polynomial R) (n : ℕ) :
+  nat_degree (hasse_deriv n p) = nat_degree p - n :=
+begin
+  cases lt_or_le p.nat_degree n with hn hn,
+  { simpa [hasse_deriv_eq_zero_of_lt_nat_degree, hn] using (tsub_eq_zero_of_le hn.le).symm },
+  { refine map_nat_degree_eq_sub _ _,
+    { exact λ h, hasse_deriv_eq_zero_of_lt_nat_degree _ _ },
+    { classical,
+      simp only [ite_eq_right_iff, ne.def, nat_degree_monomial, hasse_deriv_monomial],
+      intros k c c0 hh,
+      -- this is where we use the `smul_eq_zero` from `no_zero_smul_divisors`
+      rw [←nsmul_eq_mul, smul_eq_zero, nat.choose_eq_zero_iff] at hh,
+      exact (tsub_eq_zero_of_le (or.resolve_right hh c0).le).symm } }
+end
+
 section
 open add_monoid_hom finset.nat
 

src/data/polynomial/taylor.lean

@@ -39,9 +39,22 @@ by simp only [taylor_apply, X_comp]
 @[simp] lemma taylor_C (x : R) : taylor r (C x) = C x :=
 by simp only [taylor_apply, C_comp]
 
+@[simp] lemma taylor_zero' : taylor (0 : R) = linear_map.id :=
+begin
+  ext,
+  simp only [taylor_apply, add_zero, comp_X, _root_.map_zero, linear_map.id_comp, function.comp_app,
+             linear_map.coe_comp]
+end
+
+lemma taylor_zero (f : polynomial R) : taylor 0 f = f :=
+by rw [taylor_zero', linear_map.id_apply]
+
 @[simp] lemma taylor_one : taylor r (1 : polynomial R) = C 1 :=
 by rw [← C_1, taylor_C]
 
+@[simp] lemma taylor_monomial (i : ℕ) (k : R) : taylor r (monomial i k) = C k * (X + C r) ^ i :=
+by simp [taylor_apply]
+
 /-- The `k`th coefficient of `polynomial.taylor r f` is `(polynomial.hasse_deriv k f).eval r`. -/
 lemma taylor_coeff (n : ℕ) : (taylor r f).coeff n = (hasse_deriv n f).eval r :=
 show (lcoeff R n).comp (taylor r) f = (leval r).comp (hasse_deriv n) f,
@@ -62,10 +75,23 @@ by rw [taylor_coeff, hasse_deriv_zero, linear_map.id_apply]
 @[simp] lemma taylor_coeff_one : (taylor r f).coeff 1 = f.derivative.eval r :=
 by rw [taylor_coeff, hasse_deriv_one]
 
+@[simp] lemma nat_degree_taylor (p : polynomial R) (r : R) :
+  nat_degree (taylor r p) = nat_degree p :=
+begin
+  refine map_nat_degree_eq_nat_degree _ _,
+  nontriviality R,
+  intros n c c0,
+  simp [taylor_monomial, nat_degree_C_mul_eq_of_mul_ne_zero, nat_degree_pow_X_add_C, c0]
+end
+
 @[simp] lemma taylor_mul {R} [comm_semiring R] (r : R) (p q : polynomial R) :
   taylor r (p * q) = taylor r p * taylor r q :=
 by simp only [taylor_apply, mul_comp]
 
+lemma taylor_taylor {R} [comm_semiring R] (f : polynomial R) (r s : R) :
+  taylor r (taylor s f) = taylor (r + s) f :=
+by simp only [taylor_apply, comp_assoc, map_add, add_comp, X_comp, C_comp, C_add, add_assoc]
+
 lemma taylor_eval {R} [comm_semiring R] (r : R) (f : polynomial R) (s : R) :
   (taylor r f).eval s = f.eval (s + r) :=
 by simp only [taylor_apply, eval_comp, eval_C, eval_X, eval_add]
@@ -92,4 +118,10 @@ begin
   simp only [taylor_coeff, h, coeff_zero],
 end
 
+/-- Taylor's formula. -/
+lemma sum_taylor_eq {R} [comm_ring R] (f : polynomial R) (r : R) :
+  (taylor r f).sum (λ i a, C a * (X - C r) ^ i) = f :=
+by rw [←comp_eq_sum_left, sub_eq_add_neg, ←C_neg, ←taylor_apply, taylor_taylor, neg_add_self,
+       taylor_zero]
+
 end polynomial