PolynomialBlockInverse.lean

1 module
2 public import PolynomialWeightedInverse
3 public import PolynomialParameterSystem
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialBlockInverse
10 open Matrix Komorebi.PolynomialParameterSystem
11 open Komorebi.PolynomialWeightedInverse
12 variable {e k : ℕ} {R : Type*} [CommRing R]
13 
14 /-- An upper triangular block matrix in the original appended coordinate order. -/
15 def upperBlock (J : Matrix (Fin e) (Fin e) R)
16     (K : Matrix (Fin e) (Fin k) R) (c : R) :
17     Matrix (Fin (e + k)) (Fin (e + k)) R :=
18   join (fun i => join (J i) (K i))
19     (fun i => join 0 ((c • (1 : Matrix (Fin k) (Fin k) R)) i))
20 
21 @[simp] theorem upperBlock_solved_solved (J : Matrix (Fin e) (Fin e) R)
22     (K : Matrix (Fin e) (Fin k) R) (c : R) (i j : Fin e) :
23     upperBlock J K c (Fin.castAdd k i) (Fin.castAdd k j) = J i j := by
24   simp [upperBlock]
25 
26 @[simp] theorem upperBlock_solved_free (J : Matrix (Fin e) (Fin e) R)
27     (K : Matrix (Fin e) (Fin k) R) (c : R) (i : Fin e) (j : Fin k) :
28     upperBlock J K c (Fin.castAdd k i) (Fin.natAdd e j) = K i j := by
29   simp [upperBlock]
30 
31 @[simp] theorem upperBlock_free_solved (J : Matrix (Fin e) (Fin e) R)
32     (K : Matrix (Fin e) (Fin k) R) (c : R) (i : Fin k) (j : Fin e) :
33     upperBlock J K c (Fin.natAdd e i) (Fin.castAdd k j) = 0 := by
34   simp [upperBlock]
35 
36 @[simp] theorem upperBlock_free_free (J : Matrix (Fin e) (Fin e) R)
37     (K : Matrix (Fin e) (Fin k) R) (c : R) (i j : Fin k) :
38     upperBlock J K c (Fin.natAdd e i) (Fin.natAdd e j) =
39       (c • (1 : Matrix (Fin k) (Fin k) R)) i j := by
40   simp [upperBlock]
41 
42 /-- The block matrix acts by the expected solved and parameter formulas. -/
43 theorem upperBlock_mulVec_join (J : Matrix (Fin e) (Fin e) R)
44     (K : Matrix (Fin e) (Fin k) R) (c : R)
45     (u : Fin e → R) (v : Fin k → R) :
46     (upperBlock J K c).mulVec (join u v) =
47       join (J.mulVec u + K.mulVec v) (c • v) := by
48   ext i
49   refine Fin.addCases (fun j => ?_) (fun j => ?_) i
50   · simp [Matrix.mulVec, dotProduct, Fin.sum_univ_add]
51   · simp [Matrix.mulVec, dotProduct, Fin.sum_univ_add]
52     simp [Matrix.one_apply, mul_ite]
53 
54 /-- The integral certificate for the augmented Jacobian. -/
55 def blockCertificate (A : Matrix (Fin e) (Fin e) R)
56     (K : Matrix (Fin e) (Fin k) R) (c : R) :
57     Matrix (Fin (e + k)) (Fin (e + k)) R :=
58   upperBlock A (-(A * K)) c
59 
60 /-- A scalar left certificate transfers to the augmented system with no extra scalar loss. -/
61 theorem blockCertificate_mul (A J : Matrix (Fin e) (Fin e) R)
62     (K : Matrix (Fin e) (Fin k) R) (c : R)
63     (hAJ : A * J = c • (1 : Matrix (Fin e) (Fin e) R)) :
64     blockCertificate A K c * upperBlock J K 1 =
65       c • (1 : Matrix (Fin (e + k)) (Fin (e + k)) R) := by
66   apply Matrix.ext_iff_mulVec.mpr
67   intro v
68   rw [← join_parts v, ← Matrix.mulVec_mulVec]
69   simp only [blockCertificate, upperBlock_mulVec_join, one_smul,
70     Matrix.mulVec_add, Matrix.neg_mulVec, Matrix.mulVec_mulVec,
71     hAJ, Matrix.smul_mulVec, Matrix.one_mulVec]
72   ext i
73   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;>
74     simp [solvedPart, freePart]
75 
76 /-- A scalar right certificate also transfers to the augmented system. -/
77 theorem mul_blockCertificate (A J : Matrix (Fin e) (Fin e) R)
78     (K : Matrix (Fin e) (Fin k) R) (c : R)
79     (hJA : J * A = c • (1 : Matrix (Fin e) (Fin e) R)) :
80     upperBlock J K 1 * blockCertificate A K c =
81       c • (1 : Matrix (Fin (e + k)) (Fin (e + k)) R) := by
82   apply Matrix.ext_iff_mulVec.mpr
83   intro v
84   rw [← join_parts v, ← Matrix.mulVec_mulVec]
85   simp only [blockCertificate, upperBlock_mulVec_join, one_smul,
86     Matrix.mulVec_add, Matrix.neg_mulVec, Matrix.mulVec_neg,
87     Matrix.mulVec_smul, Matrix.mulVec_mulVec, ← Matrix.mul_assoc,
88     hJA, Matrix.smul_mul, Matrix.one_mul, Matrix.smul_mulVec, Matrix.one_mulVec]
89   ext i
90   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;>
91     simp [solvedPart, freePart]
92 
93 /-- The solved block combines coefficient motion and prescribed parameter motion with a plus sign. -/
94 theorem blockCertificate_mulVec_join_neg (A : Matrix (Fin e) (Fin e) R)
95     (K : Matrix (Fin e) (Fin k) R) (c : R)
96     (h : Fin e → R) (v : Fin k → R) :
97     (blockCertificate A K c).mulVec (join h (-v)) =
98       join (A.mulVec (h + K.mulVec v)) (-(c • v)) := by
99   simp [blockCertificate, upperBlock_mulVec_join, Matrix.mulVec_add,
100     Matrix.mulVec_mulVec, Matrix.neg_mulVec, Matrix.mulVec_neg]
101 
102 /-- Both scalar inverse identities transfer together. -/
103 theorem blockCertificate_two_sided (A J : Matrix (Fin e) (Fin e) R)
104     (K : Matrix (Fin e) (Fin k) R) (c : R)
105     (hAJ : A * J = c • (1 : Matrix (Fin e) (Fin e) R))
106     (hJA : J * A = c • (1 : Matrix (Fin e) (Fin e) R)) :
107     blockCertificate A K c * upperBlock J K 1 =
108       c • (1 : Matrix (Fin (e + k)) (Fin (e + k)) R) ∧
109     upperBlock J K 1 * blockCertificate A K c =
110       c • (1 : Matrix (Fin (e + k)) (Fin (e + k)) R) :=
111   ⟨blockCertificate_mul A J K c hAJ, mul_blockCertificate A J K c hJA⟩
112 
113 /-- The augmented inverse has the same denominator bound as the original solved inverse. -/
114 theorem bounded_inverse_upperBlock (p s : ℕ) [Fact (Nat.Prime p)]
115     (J : Matrix (Fin e) (Fin e) ℤ_[p]) (K : Matrix (Fin e) (Fin k) ℤ_[p])
116     (hJ : IsUnit (rationalMatrix p J))
117     (hA : ∃ A : Matrix (Fin e) (Fin e) ℤ_[p],
118       rationalMatrix p A = (p : ℚ_[p])^s • (rationalMatrix p J)⁻¹) :
119     IsUnit (rationalMatrix p (upperBlock J K 1)) ∧
120     ∃ C : Matrix (Fin (e + k)) (Fin (e + k)) ℤ_[p],
121       rationalMatrix p C =
122         (p : ℚ_[p])^s • (rationalMatrix p (upperBlock J K 1))⁻¹ := by
123   obtain ⟨A, hAJ, hJA⟩ := (bounded_inverse_iff_certificate p s J).mp ⟨hJ, hA⟩
124   exact (bounded_inverse_iff_certificate p s (upperBlock J K 1)).mpr
125     ⟨blockCertificate A K ((p : ℤ_[p])^s),
126       blockCertificate_two_sided A J K ((p : ℤ_[p])^s) hAJ hJA⟩
127 
128 end Komorebi.PolynomialBlockInverse

Back to source controls