PathGraphKrylov.lean

1 import KomorebiVerification.MathlibImports
2 
3 /-!
4 # Endpoint Krylov bases for path graphs
5 
6 For the path with vertices `0, ..., n`, let `A` be its adjacency operator and
7 let `e₀` be the endpoint vector.  This file proves that the walk matrix whose
8 `k`th column is `A ^ k e₀` is upper triangular with diagonal equal to one.
9 Consequently its determinant is one over every commutative ring, the first
10 `n + 1` Krylov vectors span, and `e₀` is a cyclic vector for `A`.
11 
12 Writing the number of vertices as `n + 1` makes the endpoint available without
13 an extra nonemptiness hypothesis; thus the result covers every nonempty finite
14 path, including the one-vertex path.
15 -/
16 
17 set_option autoImplicit false
18 
19 namespace Komorebi.PathGraphKrylov
20 
21 universe u
22 
23 variable (R : Type u) [CommSemiring R]
24 variable (n : ℕ)
25 
26 /-- The contribution from the neighbor immediately to the left, when it exists. -/
27 def leftTerm (x : Fin (n + 1) → R) (i : Fin (n + 1)) : R :=
28   if _h : i = 0 then
29     0
30   else
31     x ⟨i.val - 1, lt_of_le_of_lt (Nat.sub_le i.val 1) i.isLt⟩
32 
33 /-- The contribution from the neighbor immediately to the right, when it exists. -/
34 def rightTerm (x : Fin (n + 1) → R) (i : Fin (n + 1)) : R :=
35   if h : i.val < n then x ⟨i.val + 1, Nat.succ_lt_succ h⟩ else 0
36 
37 /-- The shift which reads the neighbor immediately to the left. -/
38 def leftStep : Module.End R (Fin (n + 1) → R) :=
39   LinearMap.pi fun i ↦
40     if _h : i = 0 then
41       0
42     else
43       LinearMap.proj ⟨i.val - 1, lt_of_le_of_lt (Nat.sub_le i.val 1) i.isLt⟩
44 
45 /-- The shift which reads the neighbor immediately to the right. -/
46 def rightStep : Module.End R (Fin (n + 1) → R) :=
47   LinearMap.pi fun i ↦
48     if h : i.val < n then LinearMap.proj ⟨i.val + 1, Nat.succ_lt_succ h⟩ else 0
49 
50 /-- The adjacency operator of the path `0 - 1 - ... - n`. -/
51 def pathStep : Module.End R (Fin (n + 1) → R) :=
52   leftStep R n + rightStep R n
53 
54 @[simp]
55 theorem pathStep_apply (x : Fin (n + 1) → R) (i : Fin (n + 1)) :
56     pathStep R n x i = leftTerm R n x i + rightTerm R n x i :=
57   by
58     by_cases hLeft : i = 0
59     · subst i
60       by_cases hn : 0 < n <;>
61         simp [pathStep, leftStep, rightStep, leftTerm, rightTerm, hn]
62     · by_cases hRight : i.val < n <;>
63         simp [pathStep, leftStep, rightStep, leftTerm, rightTerm, hLeft, hRight]
64 
65 /-- The standard basis vector at the left endpoint. -/
66 def endpoint : Fin (n + 1) → R :=
67   fun i ↦ if i.val = 0 then 1 else 0
68 
69 /-- The recursively presented Krylov sequence `e₀, A e₀, A² e₀, ...`. -/
70 def krylov : ℕ → Fin (n + 1) → R
71   | 0 => endpoint R n
72   | k + 1 => pathStep R n (krylov k)
73 
74 @[simp]
75 theorem krylov_zero : krylov R n 0 = endpoint R n :=
76   rfl
77 
78 @[simp]
79 theorem krylov_succ (k : ℕ) :
80     krylov R n (k + 1) = pathStep R n (krylov R n k) :=
81   rfl
82 
83 /-- The recursive Krylov sequence really is given by powers of the adjacency operator. -/
84 theorem krylov_eq_pow (k : ℕ) :
85     krylov R n k = ((pathStep R n) ^ k) (endpoint R n) := by
86   induction k with
87   | zero => simp
88   | succ k ih =>
89       rw [krylov_succ, pow_succ', Module.End.mul_apply, ih]
90 
91 /-- A walk of length `k` from `0` cannot reach a vertex strictly beyond `k`. -/
92 theorem krylov_apply_eq_zero_of_lt (k : ℕ) (i : Fin (n + 1))
93     (hki : k < i.val) : krylov R n k i = 0 := by
94   induction k generalizing i with
95   | zero =>
96       simp only [krylov_zero, endpoint]
97       simp [Nat.ne_of_gt hki]
98   | succ k ih =>
99       rw [krylov_succ, pathStep_apply]
100       have hi : 0 < i.val := by omega
101       have hi0 : i ≠ 0 := Fin.ne_of_val_ne (by simpa using Nat.ne_of_gt hi)
102       let iLeft : Fin (n + 1) :=
103         ⟨i.val - 1, lt_of_le_of_lt (Nat.sub_le i.val 1) i.isLt⟩
104       have hLeft : k < iLeft.val := by
105         dsimp [iLeft]
106         omega
107       have hzLeft : krylov R n k iLeft = 0 := ih iLeft hLeft
108       by_cases hRight : i.val < n
109       · let iRight : Fin (n + 1) := ⟨i.val + 1, Nat.succ_lt_succ hRight⟩
110         have hRight' : k < iRight.val := by
111           dsimp [iRight]
112           omega
113         have hzRight : krylov R n k iRight = 0 := ih iRight hRight'
114         simp only [leftTerm, rightTerm, hi0, hRight, dite_true, dite_false,
115           iLeft, iRight, hzLeft, hzRight, add_zero]
116       · simp only [leftTerm, rightTerm, hi0, hRight, dite_false,
117           iLeft, hzLeft, add_zero]
118 
119 /-- There is exactly one length-`k` walk from `0` to vertex `k`. -/
120 theorem krylov_diagonal (k : ℕ) (hk : k < n + 1) :
121     krylov R n k ⟨k, hk⟩ = 1 := by
122   induction k with
123   | zero => simp [krylov_zero, endpoint]
124   | succ k ih =>
125       rw [krylov_succ, pathStep_apply]
126       have hk' : k < n + 1 := by omega
127       have hne : (⟨k + 1, hk⟩ : Fin (n + 1)) ≠ 0 :=
128         Fin.ne_of_val_ne (by simp)
129       by_cases hRight : k + 1 < n
130       · let iRight : Fin (n + 1) :=
131           ⟨(k + 1) + 1, Nat.succ_lt_succ hRight⟩
132         have hlt : k < iRight.val := by
133           dsimp [iRight]
134           omega
135         have hzRight : krylov R n k iRight = 0 :=
136           krylov_apply_eq_zero_of_lt R n k iRight hlt
137         simp only [leftTerm, rightTerm, hne, hRight, dite_true, dite_false,
138           Nat.add_sub_cancel, ih hk', iRight, hzRight, add_zero]
139       · simp only [leftTerm, rightTerm, hne, hRight, dite_false,
140           Nat.add_sub_cancel, ih hk', add_zero]
141 
142 /-- The matrix of the path adjacency operator in the standard coordinate basis. -/
143 noncomputable def pathAdjacency : Matrix (Fin (n + 1)) (Fin (n + 1)) R :=
144   LinearMap.toMatrix (Pi.basisFun R (Fin (n + 1)))
145     (Pi.basisFun R (Fin (n + 1))) (pathStep R n)
146 
147 /-- Matrix multiplication by `pathAdjacency` is exactly `pathStep`. -/
148 theorem pathAdjacency_mulVec (x : Fin (n + 1) → R) :
149     (pathAdjacency R n).mulVec x = pathStep R n x := by
150   have h := LinearMap.congr_fun
151     (Matrix.toLin_toMatrix (Pi.basisFun R (Fin (n + 1)))
152       (Pi.basisFun R (Fin (n + 1))) (pathStep R n)) x
153   simpa only [pathAdjacency, Matrix.toLin_eq_toLin', Matrix.toLin'_apply] using h
154 
155 /-- Matrix powers of the adjacency matrix give the same Krylov vectors. -/
156 theorem pathAdjacency_pow_mulVec_endpoint (k : ℕ) :
157     ((pathAdjacency R n) ^ k).mulVec (endpoint R n) = krylov R n k := by
158   induction k with
159   | zero => simp [krylov_zero]
160   | succ k ih =>
161       rw [pow_succ', ← Matrix.mulVec_mulVec, ih, pathAdjacency_mulVec,
162         ← krylov_succ]
163 
164 /-- The walk matrix: column `k` is `A ^ k e₀`. -/
165 noncomputable def walkMatrix : Matrix (Fin (n + 1)) (Fin (n + 1)) R :=
166   fun i k ↦ ((pathAdjacency R n) ^ k.val).mulVec (endpoint R n) i
167 
168 theorem walkMatrix_apply (i k : Fin (n + 1)) :
169     walkMatrix R n i k = krylov R n k.val i := by
170   rw [walkMatrix, pathAdjacency_pow_mulVec_endpoint]
171 
172 /-- Entries below the diagonal of the walk matrix vanish. -/
173 theorem walkMatrix_apply_eq_zero_of_lt (i k : Fin (n + 1)) (hki : k < i) :
174     walkMatrix R n i k = 0 := by
175   rw [walkMatrix_apply]
176   exact krylov_apply_eq_zero_of_lt R n k.val i hki
177 
178 /-- Every diagonal entry of the walk matrix is one. -/
179 @[simp]
180 theorem walkMatrix_diagonal (i : Fin (n + 1)) :
181     walkMatrix R n i i = 1 := by
182   rw [walkMatrix_apply]
183   exact krylov_diagonal R n i.val i.isLt
184 
185 /-- The endpoint walk matrix is upper triangular. -/
186 theorem walkMatrix_isUpperTriangular :
187     (walkMatrix R n).IsUpperTriangular := by
188   intro i k hki
189   exact walkMatrix_apply_eq_zero_of_lt R n i k hki
190 
191 section CommRing
192 
193 variable {R : Type u} [CommRing R]
194 
195 /-- The endpoint walk matrix is unitriangular, hence has determinant one. -/
196 @[simp]
197 theorem walkMatrix_det : (walkMatrix R n).det = 1 := by
198   rw [Matrix.det_of_isUpperTriangular (walkMatrix_isUpperTriangular R n)]
199   simp
200 
201 /-- The finite endpoint Krylov family spans the whole coordinate module. -/
202 theorem krylov_span_eq_top :
203     Submodule.span R (Set.range fun k : Fin (n + 1) ↦ krylov R n k.val) = ⊤ := by
204   have hdet : IsUnit (walkMatrix R n).det := by
205     rw [walkMatrix_det]
206     exact isUnit_one
207   have hrange : LinearMap.range (Matrix.toLin' (walkMatrix R n)) = ⊤ := by
208     rw [← Matrix.toLin_eq_toLin']
209     exact Matrix.range_toLin_eq_top (Pi.basisFun R (Fin (n + 1)))
210       (walkMatrix R n) hdet
211   rw [Matrix.range_toLin'] at hrange
212   have hcol : (walkMatrix R n).col =
213       (fun k : Fin (n + 1) ↦ krylov R n k.val) := by
214     funext k i
215     exact walkMatrix_apply R n i k
216   rwa [hcol] at hrange
217 
218 /-- A vector is cyclic for an operator when the span of all of its iterates is the top module. -/
219 def IsCyclic (T : Module.End R (Fin (n + 1) → R))
220     (x : Fin (n + 1) → R) : Prop :=
221   Submodule.span R (Set.range fun k : ℕ ↦ (T ^ k) x) = ⊤
222 
223 /-- The left endpoint is cyclic for the path adjacency operator. -/
224 theorem endpoint_isCyclic :
225     IsCyclic (R := R) n (pathStep R n) (endpoint R n) := by
226   rw [IsCyclic]
227   apply le_antisymm le_top
228   rw [← krylov_span_eq_top (R := R) n]
229   apply Submodule.span_mono
230   rintro _ ⟨k, rfl⟩
231   refine ⟨k.val, ?_⟩
232   exact (krylov_eq_pow R n k.val).symm
233 
234 end CommRing
235 
236 end Komorebi.PathGraphKrylov
237 
238 #print axioms Komorebi.PathGraphKrylov.endpoint_isCyclic

Back to source controls