PolynomialMotionRational.lean

1 module
2 public import PolynomialWeightedInverse
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialMotionRational
9 open Matrix Komorebi.PolynomialWeightedInverse
10 variable {d : ℕ}
11 
12 /-- The inclusion of integral p-adic vectors commutes with matrix multiplication. -/
13 theorem coe_mulVec (p : ℕ) [Fact (Nat.Prime p)]
14     (A : Matrix (Fin d) (Fin d) ℤ_[p]) (v : Fin d → ℤ_[p]) :
15     (fun i => (A.mulVec v i : ℚ_[p])) =
16       (rationalMatrix p A).mulVec (fun i => (v i : ℚ_[p])) := by
17   ext i
18   simp [Matrix.mulVec, dotProduct, rationalMatrix]
19 
20 /-- The integral correction using a scaled inverse is exactly the rational Newton correction. -/
21 theorem scaled_inverse_mulVec (p s M : ℕ) [Fact (Nat.Prime p)] (hMs : s ≤ M)
22     (J A : Matrix (Fin d) (Fin d) ℤ_[p])
23     (hA : rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹)
24     (v : Fin d → ℤ_[p]) (i : Fin d) :
25     (((p : ℤ_[p])^(M-s) * A.mulVec v i : ℤ_[p]) : ℚ_[p]) =
26       (p : ℚ_[p])^M * ((rationalMatrix p J)⁻¹).mulVec
27         (fun j => (v j : ℚ_[p])) i := by
28   have hv := congrFun (coe_mulVec p A v) i
29   rw [hA, Matrix.smul_mulVec] at hv
30   simp only [Pi.smul_apply, smul_eq_mul] at hv
31   push_cast
32   rw [hv, ← mul_assoc, ← pow_add, Nat.sub_add_cancel hMs]
33 
34 /-- A divisibility estimate on the integral correction yields the written first-order
35 formula over the fraction field, with an integral error of exactly the same depth. -/
36 theorem exists_rational_error (p s M N : ℕ) [Fact (Nat.Prime p)] (hMs : s ≤ M)
37     (J A : Matrix (Fin d) (Fin d) ℤ_[p])
38     (hA : rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹)
39     (a b v : Fin d → ℤ_[p])
40     (herror : ∀ i, (p : ℤ_[p])^N ∣ b i - a i + (p : ℤ_[p])^(M-s) * A.mulVec v i) :
41     ∃ ε : Fin d → ℤ_[p], (∀ i, (p : ℤ_[p])^N ∣ ε i) ∧
42       ∀ i, (b i : ℚ_[p]) - (a i : ℚ_[p]) =
43         -(p : ℚ_[p])^M * ((rationalMatrix p J)⁻¹).mulVec
44           (fun j => (v j : ℚ_[p])) i + (ε i : ℚ_[p]) := by
45   refine ⟨fun i => b i - a i + (p : ℤ_[p])^(M-s) * A.mulVec v i, herror, ?_⟩
46   intro i
47   have hscale := scaled_inverse_mulVec p s M hMs J A hA v i
48   push_cast at hscale ⊢
49   rw [hscale]
50   ring
51 
52 end Komorebi.PolynomialMotionRational

Back to source controls