PolynomialTaylorDisplacement.lean

1 module
2 public import PolynomialTaylorRing
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialTaylorDisplacement
9 open scoped BigOperators
10 open MvPolynomial
11 variable {R : Type*} [CommRing R] {d : ℕ}
12 
13 /-- The Taylor error is divisible by the square of any common divisor of the
14 actual coordinate displacement. The Jacobian entries are evaluated derivatives. -/
15 theorem taylor_remainder_dvd (P : MvPolynomial (Fin d) R)
16     (a b : Fin d → R) (c : R) (h : ∀ i, c ∣ b i - a i) :
17     c ^ 2 ∣ eval b P - eval a P -
18       ∑ i, eval a (pderiv i P) * (b i - a i) := by
19   choose u hu using h
20   have hb : b = fun i => a i + c * u i := by
21     funext i
22     linear_combination hu i
23   obtain ⟨Q, hQ, _⟩ := PolynomialTaylorRing.exists_eval_scaled_remainder P a c
24   have hsum : (∑ i, eval a (pderiv i P) * (b i - a i)) =
25       c * (∑ i, eval a (pderiv i P) * u i) := by
26     rw [Finset.mul_sum]
27     apply Finset.sum_congr rfl
28     intro i _
29     rw [hu i]
30     ring
31   refine ⟨eval u Q, ?_⟩
32   rw [hsum, hb, hQ]
33   ring
34 
35 end Komorebi.PolynomialTaylorDisplacement

Back to source controls