PolynomialWeightedNormalization.lean

1 module
2 
3 public import PolynomialTaylorRing
4 public import PolynomialWeightedInverse
5 
6 @[expose] public section
7 
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PolynomialWeightedNormalization
12 
13 open scoped BigOperators
14 open MvPolynomial
15 open Komorebi.PolynomialTaylorRing Komorebi.PolynomialWeightedInverse
16 
17 variable {d : ℕ}
18 
19 /-- The actual linear Taylor term of the preconditioned system is scalar multiplication. -/
20 theorem precondition_directional (p s : ℕ) [Fact (Nat.Prime p)]
21     (F : Fin d → MvPolynomial (Fin d) ℤ_[p]) (a : Fin d → ℤ_[p])
22     (A : Matrix (Fin d) (Fin d) ℤ_[p])
23     (hAJ : A * jacobian F a = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
24     (u : Fin d → ℤ_[p]) (i : Fin d) :
25     (∑ j, eval a (pderiv j (precondition A F i)) * u j) = (p : ℤ_[p]) ^ s * u i := by
26   change (jacobian (precondition A F) a).mulVec u i = _
27   rw [jacobian_precondition, hAJ, Matrix.smul_mulVec, Matrix.one_mulVec]
28   rfl
29 
30 /-- The actual nonlinear system admits an integral contraction normalization. The
31 remainder vanishes at zero, and the constant retains the exact excess residual precision. -/
32 theorem exists_normalization (p s r : ℕ) [Fact (Nat.Prime p)] (hr : 2 * s < r)
33     (F : Fin d → MvPolynomial (Fin d) ℤ_[p]) (a : Fin d → ℤ_[p])
34     (A : Matrix (Fin d) (Fin d) ℤ_[p])
35     (hAJ : A * jacobian F a = (p : ℤ_[p]) ^ s • (1 : Matrix (Fin d) (Fin d) ℤ_[p]))
36     (hF : ∀ i, (p : ℤ_[p]) ^ r ∣ eval a (F i)) :
37     ∃ C₀ : Fin d → ℤ_[p], ∃ Q : Fin d → MvPolynomial (Fin d) ℤ_[p],
38       (∀ i, (p : ℤ_[p]) ^ (r - (2 * s + 1)) ∣ C₀ i) ∧
39       (∀ i, eval (0 : Fin d → ℤ_[p]) (Q i) = 0) ∧
40       (∀ (u : Fin d → ℤ_[p]) i,
41         eval (fun j => a j + (p : ℤ_[p]) ^ (s + 1) * u j) (precondition A F i) =
42           (p : ℤ_[p]) ^ (2 * s + 1) *
43             (C₀ i + u i + (p : ℤ_[p]) * eval u (Q i))) := by
44   have hAF : ∀ i, (p : ℤ_[p]) ^ r ∣ eval a (precondition A F i) := by
45     intro i
46     have h := mulVec_preserves_dvd A ((p : ℤ_[p]) ^ r)
47       (fun j => eval a (F j)) hF i
48     rw [← eval_precondition A F a] at h
49     exact h
50   choose D hD using hAF
51   choose Q hQ hQ0 using fun i => exists_eval_scaled_remainder
52     (precondition A F i) a ((p : ℤ_[p]) ^ (s + 1))
53   refine ⟨fun i => (p : ℤ_[p]) ^ (r - (2 * s + 1)) * D i, Q,
54     fun i => dvd_mul_right _ _, hQ0, ?_⟩
55   intro u i
56   rw [hQ i u, hD i, precondition_directional p s F a A hAJ]
57   have hpow₀ : (p : ℤ_[p]) ^ (2 * s + 1) * (p : ℤ_[p]) ^ (r - (2 * s + 1)) =
58       (p : ℤ_[p]) ^ r := by
59     rw [← pow_add, Nat.add_sub_of_le (by omega)]
60   have hpow₁ : (p : ℤ_[p]) ^ (s + 1) * (p : ℤ_[p]) ^ s =
61       (p : ℤ_[p]) ^ (2 * s + 1) := by
62     rw [← pow_add]
63     congr 1
64     omega
65   have hpow₂ : ((p : ℤ_[p]) ^ (s + 1)) ^ 2 =
66       (p : ℤ_[p]) ^ (2 * s + 1) * (p : ℤ_[p]) := by
67     rw [← pow_mul, ← pow_succ]
68     congr 1
69     omega
70   rw [hpow₂]
71   linear_combination -(D i) * hpow₀ + (u i) * hpow₁
72 
73 end Komorebi.PolynomialWeightedNormalization

Back to source controls