PolynomialJointDeformation.lean

1 module
2 public import PolynomialJointMotion
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialJointDeformation
9 open MvPolynomial Matrix
10 open Komorebi.PolynomialParameterSystem (join solvedPart freePart)
11 open Komorebi.PolynomialWeightedInverse
12 open Komorebi.PolynomialJointSystem (solvedJacobian parameterJacobian)
13 
14 variable {e k : ℕ}
15 
16 /-- A solved-coordinate point in the weighted uniqueness ball, combined with
17 its prescribed parameter displacement, lies in the full augmented ball. -/
18 theorem join_deformed_ball (p s M : ℕ) [Fact (Nat.Prime p)] (hM : 2 * s < M)
19     (a : Fin (e+k) → ℤ_[p]) (v : Fin k → ℤ_[p]) (y : Fin e → ℤ_[p])
20     (hy : ∀ i, (p : ℤ_[p])^(s+1) ∣ y i - solvedPart a i) :
21     ∀ i, (p : ℤ_[p])^(s+1) ∣
22       join y (freePart a + (p : ℤ_[p])^M • v) i - a i := by
23   intro i
24   refine Fin.addCases (fun j => ?_) (fun j => ?_) i
25   · simpa only [PolynomialParameterSystem.join_solved, solvedPart] using hy j
26   · simp only [PolynomialParameterSystem.join_free, Pi.add_apply, Pi.smul_apply,
27       smul_eq_mul, freePart, add_sub_cancel_left]
28     exact dvd_mul_of_dvd_left (pow_dvd_pow (p : ℤ_[p]) (by omega)) (v j)
29 
30 /-- The joint deformation theorem in the original solved-coordinate variables.
31 The only inverse assumption concerns the original actual solved Jacobian. -/
32 theorem exists_joint_deformation (p s M : ℕ) [Fact (Nat.Prime p)]
33     (hM : 2 * s < M) (F H : Fin e → MvPolynomial (Fin (e+k)) ℤ_[p])
34     (a : Fin (e+k) → ℤ_[p]) (hFa : ∀ i, eval a (F i) = 0)
35     (hJ : IsUnit (rationalMatrix p (solvedJacobian F a)))
36     (hbound : ∃ A : Matrix (Fin e) (Fin e) ℤ_[p],
37       rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p (solvedJacobian F a))⁻¹)
38     (v : Fin k → ℤ_[p]) :
39     ∃ y : Fin e → ℤ_[p],
40       (∀ i, eval (join y (freePart a + (p : ℤ_[p])^M • v)) (F i) +
41         (p : ℤ_[p])^M * eval (join y (freePart a + (p : ℤ_[p])^M • v)) (H i) = 0) ∧
42       (∀ i, (p : ℤ_[p])^(M-s) ∣ y i - solvedPart a i) ∧
43       (∀ i, (p : ℤ_[p])^(s+1) ∣ y i - solvedPart a i) ∧
44       (∀ z : Fin e → ℤ_[p],
45         (∀ i, eval (join z (freePart a + (p : ℤ_[p])^M • v)) (F i) +
46           (p : ℤ_[p])^M * eval (join z (freePart a + (p : ℤ_[p])^M • v)) (H i) = 0) →
47         (∀ i, (p : ℤ_[p])^(s+1) ∣ z i - solvedPart a i) → z = y) ∧
48       (∃ ε : Fin e → ℤ_[p], (∀ i, (p : ℤ_[p])^(2*M-3*s) ∣ ε i) ∧
49         ∀ i, (y i : ℚ_[p]) - (a (Fin.castAdd k i) : ℚ_[p]) =
50           -(p : ℚ_[p])^M * ((rationalMatrix p (solvedJacobian F a))⁻¹).mulVec
51             (fun j => ((eval a (H j) + (parameterJacobian F a).mulVec v j : ℤ_[p]) : ℚ_[p])) i +
52           (ε i : ℚ_[p])) := by
53   obtain ⟨b, hb, hbparams, hdepth, hball, huniq, herror⟩ :=
54     PolynomialJointMotion.exists_joint_root_motion p s M hM F H a v hFa hJ hbound
55   have hjoin : join (solvedPart b) (freePart a + (p : ℤ_[p])^M • v) = b := by
56     rw [← hbparams, PolynomialParameterSystem.join_parts]
57   refine ⟨solvedPart b, ?_, ?_, ?_, ?_, herror⟩
58   · simpa only [hjoin] using hb
59   · exact fun i => hdepth (Fin.castAdd k i)
60   · exact fun i => hball (Fin.castAdd k i)
61   · intro z hz hzb
62     have hfull := huniq (join z (freePart a + (p : ℤ_[p])^M • v)) hz
63       (PolynomialParameterSystem.freePart_join _ _)
64       (join_deformed_ball p s M hM a v z hzb)
65     simpa only [PolynomialParameterSystem.solvedPart_join] using
66       congrArg (fun w : Fin (e+k) → ℤ_[p] => solvedPart w) hfull
67 
68 /-- Unique existence holds throughout the original solved-coordinate ball. -/
69 theorem exists_unique_joint_deformation (p s M : ℕ) [Fact (Nat.Prime p)]
70     (hM : 2 * s < M) (F H : Fin e → MvPolynomial (Fin (e+k)) ℤ_[p])
71     (a : Fin (e+k) → ℤ_[p]) (hFa : ∀ i, eval a (F i) = 0)
72     (hJ : IsUnit (rationalMatrix p (solvedJacobian F a)))
73     (hbound : ∃ A : Matrix (Fin e) (Fin e) ℤ_[p],
74       rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p (solvedJacobian F a))⁻¹)
75     (v : Fin k → ℤ_[p]) :
76     ∃! y : Fin e → ℤ_[p],
77       (∀ i, eval (join y (freePart a + (p : ℤ_[p])^M • v)) (F i) +
78         (p : ℤ_[p])^M * eval (join y (freePart a + (p : ℤ_[p])^M • v)) (H i) = 0) ∧
79       (∀ i, (p : ℤ_[p])^(s+1) ∣ y i - solvedPart a i) := by
80   obtain ⟨y, hy, _, hball, huniq, _⟩ :=
81     exists_joint_deformation p s M hM F H a hFa hJ hbound v
82   exact ⟨y, ⟨hy, hball⟩, fun z hz => huniq z hz.1 hz.2⟩
83 
84 end Komorebi.PolynomialJointDeformation

Back to source controls