PolynomialTaylorRing.lean

1 module
2 
3 public import Mathlib.Algebra.MvPolynomial.PDeriv
4 public import Mathlib.Algebra.MvPolynomial.Monad
5 public import Mathlib.Tactic
6 
7 @[expose] public section
8 
9 noncomputable section
10 set_option autoImplicit false
11 
12 namespace Komorebi.PolynomialTaylorRing
13 
14 open scoped BigOperators
15 open MvPolynomial
16 
17 variable {R : Type*} [CommRing R] {d : ℕ}
18 
19 /-- The polynomial linear part formed from the actual partial derivatives. -/
20 def linearPart (P : MvPolynomial (Fin d) R) (a : Fin d → R) :
21     MvPolynomial (Fin d) R :=
22   ∑ i, C (eval a (pderiv i P)) * X i
23 
24 @[simp] theorem linearPart_C (r : R) (a : Fin d → R) :
25     linearPart (C r) a = 0 := by
26   simp [linearPart]
27 
28 @[simp] theorem linearPart_add (P Q : MvPolynomial (Fin d) R) (a : Fin d → R) :
29     linearPart (P + Q) a = linearPart P a + linearPart Q a := by
30   simp [linearPart, map_add, add_mul, Finset.sum_add_distrib]
31 
32 theorem linearPart_mul (P Q : MvPolynomial (Fin d) R) (a : Fin d → R) :
33     linearPart (P * Q) a = linearPart P a * C (eval a Q) +
34       C (eval a P) * linearPart Q a := by
35   simp only [linearPart, pderiv_mul, map_add, map_mul, add_mul,
36     Finset.sum_add_distrib, Finset.sum_mul, Finset.mul_sum]
37   congr 1 <;> apply Finset.sum_congr rfl <;> intro i hi <;> ring
38 
39 @[simp] theorem linearPart_X (j : Fin d) (a : Fin d → R) :
40     linearPart (X j) a = X j := by
41   classical
42   simp [linearPart, pderiv_X, Pi.single_apply, apply_ite]
43 
44 @[simp] theorem eval_zero_linearPart (P : MvPolynomial (Fin d) R) (a : Fin d → R) :
45     eval (0 : Fin d → R) (linearPart P a) = 0 := by
46   simp [linearPart]
47 
48 @[simp] theorem eval_linearPart (P : MvPolynomial (Fin d) R) (a u : Fin d → R) :
49     eval u (linearPart P a) = ∑ i, eval a (pderiv i P) * u i := by
50   simp [linearPart]
51 
52 /-- Polynomial Taylor normalization, with a polynomial remainder whose constant term is zero. -/
53 theorem exists_scaled_remainder (P : MvPolynomial (Fin d) R) (a : Fin d → R) (c : R) :
54     ∃ Q : MvPolynomial (Fin d) R,
55       bind₁ (fun i => C (a i) + C c * X i) P =
56         C (eval a P) + C c * linearPart P a + C (c ^ 2) * Q ∧
57       eval (0 : Fin d → R) Q = 0 := by
58   induction P using MvPolynomial.induction_on with
59   | C r => exact ⟨0, by simp, by simp⟩
60   | add P S hP hS =>
61     obtain ⟨Q, hQ, hQ0⟩ := hP
62     obtain ⟨T, hT, hT0⟩ := hS
63     refine ⟨Q + T, ?_, by simp only [map_add, hQ0, hT0, add_zero]⟩
64     simp only [map_add, linearPart_add]
65     rw [hQ, hT]
66     ring
67   | mul_X P j hP =>
68     obtain ⟨Q, hQ, hQ0⟩ := hP
69     refine ⟨Q * (C (a j) + C c * X j) + linearPart P a * X j, ?_, ?_⟩
70     · simp only [map_mul, bind₁_X_right, eval_X, linearPart_mul, linearPart_X]
71       rw [hQ]
72       simp only [map_pow]
73       ring
74     · simp only [map_add, map_mul, eval_C, eval_X, Pi.zero_apply, hQ0,
75         mul_zero, add_zero, zero_mul]
76 
77 /-- Evaluation of the scaled substitution. -/
78 theorem eval_scaled_bind (P : MvPolynomial (Fin d) R) (a u : Fin d → R) (c : R) :
79     eval u (bind₁ (fun i => C (a i) + C c * X i) P) =
80       eval (fun i => a i + c * u i) P := by
81   change eval₂Hom (RingHom.id R) u (bind₁ _ P) = _
82   rw [eval₂Hom_bind₁]
83   simp only [map_add, map_mul, eval₂Hom_C, eval₂Hom_X', RingHom.id_apply]
84   rfl
85 
86 /-- The same remainder works at every point, rather than being chosen after evaluation. -/
87 theorem exists_eval_scaled_remainder (P : MvPolynomial (Fin d) R)
88     (a : Fin d → R) (c : R) :
89     ∃ Q : MvPolynomial (Fin d) R,
90       (∀ u : Fin d → R, eval (fun i => a i + c * u i) P =
91         eval a P + c * (∑ i, eval a (pderiv i P) * u i) + c ^ 2 * eval u Q) ∧
92       eval (0 : Fin d → R) Q = 0 := by
93   obtain ⟨Q, hQ, hQ0⟩ := exists_scaled_remainder P a c
94   refine ⟨Q, ?_, hQ0⟩
95   intro u
96   have h := congrArg (eval u) hQ
97   simpa only [eval_scaled_bind, map_add, map_mul, eval_C, eval_linearPart] using h
98 
99 /-- Polynomial evaluation respects divisibility of all coordinate differences over any commutative ring. -/
100 theorem eval_dvd_of_dvd (P : MvPolynomial (Fin d) R) (x y : Fin d → R)
101     (c : R) (h : ∀ i, c ∣ y i - x i) :
102     c ∣ eval y P - eval x P := by
103   induction P using MvPolynomial.induction_on with
104   | C r => simp
105   | add P Q hP hQ =>
106     simp only [map_add]
107     convert dvd_add hP hQ using 2
108     ring
109   | mul_X P j hP =>
110     obtain ⟨r, hr⟩ := hP
111     obtain ⟨s, hs⟩ := h j
112     refine ⟨r * y j + eval x P * s, ?_⟩
113     simp only [map_mul, eval_X]
114     linear_combination y j * hr + eval x P * hs
115 
116 end Komorebi.PolynomialTaylorRing

Back to source controls