PolynomialTaylor.lean

1 module
2 
3 public import Mathlib.Algebra.MvPolynomial.PDeriv
4 public import Mathlib.Tactic
5 
6 @[expose] public section
7 
8 namespace Komorebi.PolynomialTaylor
9 
10 open scoped BigOperators
11 open MvPolynomial
12 
13 /-- The actual directional derivative formed from the partial derivatives. -/
14 noncomputable def directional {d : ℕ} (P : MvPolynomial (Fin d) ℤ)
15     (x t : Fin d → ℤ) : ℤ :=
16   ∑ i, eval x (pderiv i P) * t i
17 
18 theorem directional_C {d : ℕ} (c : ℤ) (x t : Fin d → ℤ) :
19     directional (C c) x t = 0 := by
20   simp [directional]
21 
22 theorem directional_add {d : ℕ} (P Q : MvPolynomial (Fin d) ℤ)
23     (x t : Fin d → ℤ) :
24     directional (P + Q) x t = directional P x t + directional Q x t := by
25   simp [directional, map_add, add_mul, Finset.sum_add_distrib]
26 
27 theorem directional_mul {d : ℕ} (P Q : MvPolynomial (Fin d) ℤ)
28     (x t : Fin d → ℤ) :
29     directional (P * Q) x t =
30       directional P x t * eval x Q + eval x P * directional Q x t := by
31   simp only [directional, pderiv_mul, map_add, map_mul, add_mul,
32     Finset.sum_add_distrib, Finset.sum_mul, Finset.mul_sum]
33   congr 1 <;> apply Finset.sum_congr rfl <;> intro i hi <;> ring
34 
35 theorem directional_X {d : ℕ} (j : Fin d) (x t : Fin d → ℤ) :
36     directional (X j) x t = t j := by
37   classical
38   simp [directional, pderiv_X, Pi.single_apply, apply_ite]
39 
40 /-- Integral first-order Taylor formula, with an actual divisible remainder. -/
41 theorem taylor_dvd {d : ℕ} (P : MvPolynomial (Fin d) ℤ)
42     (x t : Fin d → ℤ) (a : ℤ) :
43     a ^ 2 ∣ eval (fun i => x i + a * t i) P - eval x P - a * directional P x t := by
44   induction P using MvPolynomial.induction_on with
45   | C c => simp [directional]
46   | add P Q hP hQ =>
47     simp only [map_add, directional_add]
48     convert dvd_add hP hQ using 2 <;> first | rfl | ring
49   | mul_X P j hP =>
50     obtain ⟨r, hr⟩ := hP
51     refine ⟨r * (x j + a * t j) + directional P x t * t j, ?_⟩
52     simp only [map_mul, eval_X, directional_mul, directional_X]
53     linear_combination (x j + a * t j) * hr
54 
55 /-- At positive depth the quadratic remainder vanishes at the next precision. -/
56 theorem taylor_step_dvd {d : ℕ} (P : MvPolynomial (Fin d) ℤ)
57     (x t : Fin d → ℤ) (q L : ℕ) (hL : 1 ≤ L) :
58     (q : ℤ) ^ (L + 1) ∣
59       eval (fun i => x i + (q : ℤ) ^ L * t i) P - eval x P -
60         (q : ℤ) ^ L * directional P x t := by
61   apply dvd_trans (b := ((q : ℤ) ^ L) ^ 2) ?_ (taylor_dvd P x t _)
62   rw [← pow_mul]
63   exact pow_dvd_pow _ (by omega)
64 
65 /-- Integral polynomial evaluation respects every coordinate congruence. -/
66 theorem eval_dvd_of_dvd {d : ℕ} (P : MvPolynomial (Fin d) ℤ)
67     (x y : Fin d → ℤ) (a : ℤ) (h : ∀ i, a ∣ y i - x i) :
68     a ∣ eval y P - eval x P := by
69   induction P using MvPolynomial.induction_on with
70   | C c => simp
71   | add P Q hP hQ =>
72     simp only [map_add]
73     convert dvd_add hP hQ using 2 <;> first | rfl | ring
74   | mul_X P j hP =>
75     obtain ⟨r, hr⟩ := hP
76     obtain ⟨s, hs⟩ := h j
77     refine ⟨r * y j + eval x P * s, ?_⟩
78     simp only [map_mul, eval_X]
79     linear_combination y j * hr + eval x P * hs
80 
81 /-- In particular, an integral Jacobian is constant modulo the base modulus. -/
82 theorem pderiv_eval_dvd_of_dvd {d : ℕ} (P : MvPolynomial (Fin d) ℤ)
83     (x y : Fin d → ℤ) (a : ℤ) (h : ∀ i, a ∣ y i - x i) (j : Fin d) :
84     a ∣ eval y (pderiv j P) - eval x (pderiv j P) :=
85   eval_dvd_of_dvd (pderiv j P) x y a h
86 
87 end Komorebi.PolynomialTaylor

Back to source controls