ReleaseTransferScalar.lean

1 import KomorebiVerification.PaperII.TransferZeta
2 import KomorebiVerification.PaperII.ReleaseTransferMatrix
3 /-!
4 Scalar-weighted semantic walks. The finite walk type is the original unrestricted
5 list model with its proved finite enumeration. Products below retain every edge
6 occurrence, including parallel edges and repeated visits.
7 -/
8 set_option autoImplicit false
9 open scoped BigOperators
10 
11 namespace Komorebi.PaperII.ReleaseTransferScalar
12 open TransferZeta TransferZeta.PositiveWeightedMultigraph
13 universe u v w
14 variable {V : Type u} {E : Type v} {R : Type w}
15 variable [Fintype E] [DecidableEq V] [CommRing R]
16 variable (G : PositiveWeightedMultigraph V E) (m : E → R)
17 
18 def walkMultiplicity (es : List E) : R := (es.map m).prod
19 
20 omit [Fintype E] in
21 @[simp] theorem walkMultiplicity_nil : walkMultiplicity m [] = 1 := rfl
22 omit [Fintype E] in
23 @[simp] theorem walkMultiplicity_cons (e : E) (es : List E) :
24     walkMultiplicity m (e :: es) = m e * walkMultiplicity m es := rfl
25 
26 noncomputable def coefficient (s t : V) (n : ℕ) : R :=
27   ∑ x : G.ExactWalk s t n, walkMultiplicity m x.val
28 
29 theorem coefficient_firstEdge (s t : V) (n : ℕ) :
30     coefficient G m s t n = (if s = t ∧ n = 0 then 1 else 0) +
31       ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
32         m e * coefficient G m (G.target e) t (n - G.weight e) else 0 := by
33   classical
34   let f : EmptyExactWalk s t n ⊕ G.FirstEdgeExactWalk s t n → R :=
35     Sum.elim (fun _ ↦ 1) (fun x ↦ m x.val.1 * walkMultiplicity m x.val.2)
36   have hfirst : coefficient G m s t n = ∑ x, f x := by
37     apply Fintype.sum_equiv (G.exactWalkFirstEdgeEquiv s t n)
38     intro x
39     rcases x with ⟨es, hx⟩
40     cases es <;> rfl
41   rw [hfirst, Fintype.sum_sum_type]
42   have hempty : (∑ _x : EmptyExactWalk s t n, (1 : R)) =
43       if s = t ∧ n = 0 then 1 else 0 := by
44     by_cases h : s = t ∧ n = 0 <;> simp [EmptyExactWalk, h]
45   change (∑ _x : EmptyExactWalk s t n, (1 : R)) +
46     (∑ x : G.FirstEdgeExactWalk s t n, m x.val.1 * walkMultiplicity m x.val.2) = _
47   rw [hempty]
48   congr 1
49   calc
50     _ = ∑ x : G.FirstEdgeTail s t n,
51           m x.1 * walkMultiplicity m x.2.val.val := by
52       apply Fintype.sum_equiv (G.firstEdgeTailEquiv s t n)
53       intro x
54       rcases x with ⟨⟨e, es⟩, hs, hw, hn⟩
55       rfl
56     _ = _ := by
57       rw [Fintype.sum_sigma]
58       apply Finset.sum_congr rfl
59       intro e _
60       by_cases h : G.source e = s ∧ G.weight e ≤ n
61       · rw [ite_eq_left h, coefficient, Finset.mul_sum]
62         apply Fintype.sum_equiv (Equiv.subtypeUnivEquiv fun _ ↦ h)
63         intro x
64         rfl
65       · rw [ite_eq_right h]
66         apply Finset.sum_eq_zero
67         intro x _
68         exact False.elim (h x.property)
69 
70 noncomputable def series (s t : V) : PowerSeries R :=
71   PowerSeries.mk (coefficient G m s t)
72 
73 @[simp] theorem coeff_series (s t : V) (n : ℕ) :
74     PowerSeries.coeff n (series G m s t) = coefficient G m s t n := by
75   simp [series]
76 
77 noncomputable def adjacency : Matrix V V (Polynomial R) :=
78   fun i j ↦ ∑ e : E, if G.source e = i ∧ G.target e = j then
79     Polynomial.monomial (G.weight e) (m e) else 0
80 
81 theorem adjacency_coeff_zero (i j : V) : (adjacency G m i j).coeff 0 = 0 := by
82   classical
83   rw [adjacency, ← Polynomial.lcoeff_apply, map_sum]
84   simp only [Polynomial.lcoeff_apply]
85   apply Finset.sum_eq_zero
86   intro e _
87   by_cases h : G.source e = i ∧ G.target e = j
88   · simp [h, Polynomial.coeff_monomial, Nat.ne_of_gt (G.weight_pos e)]
89   · simp [h]
90 
91 
92 
93 variable [Fintype V]
94 
95 noncomputable def adjacencySeries : Matrix V V (PowerSeries R) :=
96   Polynomial.coeToPowerSeries.ringHom.mapMatrix (adjacency G m)
97 
98 noncomputable def seriesMatrix : Matrix V V (PowerSeries R) := fun s t ↦ series G m s t
99 
100 theorem adjacencySeries_mul_seriesMatrix_apply (s t : V) :
101     (adjacencySeries G m * seriesMatrix G m) s t =
102       ∑ e : E, if G.source e = s then
103         (PowerSeries.C (m e) * PowerSeries.X ^ G.weight e) *
104           series G m (G.target e) t else 0 := by
105   classical
106   have hmon (e : E) :
107       ((Polynomial.monomial (G.weight e) (m e) : Polynomial R) : PowerSeries R) =
108         PowerSeries.C (m e) * PowerSeries.X ^ G.weight e := by
109     ext n
110     simp [PowerSeries.coeff_monomial]
111   have hadj (i j : V) : adjacencySeries G m i j =
112       ∑ e : E, if G.source e = i ∧ G.target e = j then
113         (PowerSeries.C (m e) * PowerSeries.X ^ G.weight e) else 0 := by
114     rw [adjacencySeries, RingHom.mapMatrix_apply, Matrix.map_apply, adjacency, map_sum]
115     apply Finset.sum_congr rfl
116     intro e _
117     by_cases h : G.source e = i ∧ G.target e = j <;> simp [h, hmon]
118   rw [Matrix.mul_apply]
119   simp_rw [hadj, Finset.sum_mul]
120   rw [Finset.sum_comm]
121   apply Finset.sum_congr rfl
122   intro e _
123   by_cases hs : G.source e = s
124   · simp [hs, seriesMatrix]
125   · simp [hs]
126 
127 theorem coeff_adjacency_mul_series (s t : V) (n : ℕ) :
128     PowerSeries.coeff n ((adjacencySeries G m * seriesMatrix G m) s t) =
129       ∑ e : E, if G.source e = s ∧ G.weight e ≤ n then
130         m e * coefficient G m (G.target e) t (n - G.weight e) else 0 := by
131   classical
132   rw [adjacencySeries_mul_seriesMatrix_apply, map_sum]
133   apply Finset.sum_congr rfl
134   intro e _
135   by_cases hs : G.source e = s
136   · by_cases hw : G.weight e ≤ n <;>
137       simp [hs, hw, mul_assoc, PowerSeries.coeff_C_mul, PowerSeries.coeff_X_pow_mul']
138   · simp [hs]
139 
140 theorem seriesMatrix_eq_one_add_adjacency_mul :
141     seriesMatrix G m = 1 + adjacencySeries G m * seriesMatrix G m := by
142   ext s t n
143   change PowerSeries.coeff n (series G m s t) =
144     PowerSeries.coeff n ((1 : Matrix V V (PowerSeries R)) s t +
145       (adjacencySeries G m * seriesMatrix G m) s t)
146   rw [coeff_series, map_add, coeff_adjacency_mul_series]
147   have hrec := coefficient_firstEdge G m s t n
148   by_cases hst : s = t
149   · subst t
150     by_cases hn : n = 0 <;> simpa [Matrix.one_apply, PowerSeries.coeff_one, hn] using hrec
151   · simpa [Matrix.one_apply, PowerSeries.coeff_one, hst] using hrec
152 
153 noncomputable def transfer : Matrix V V (Polynomial R) := 1 - adjacency G m
154 noncomputable def denominator : Polynomial R := Matrix.det (transfer G m)
155 noncomputable def denominatorInverse : PowerSeries R :=
156   PowerSeries.invOfUnit (denominator G m : PowerSeries R) (1 : Rˣ)
157 
158 theorem denominator_coeff_zero : (denominator G m).coeff 0 = 1 := by
159   change Polynomial.constantCoeff (denominator G m) = 1
160   rw [denominator, RingHom.map_det]
161   have h : Polynomial.constantCoeff.mapMatrix (transfer G m) = (1 : Matrix V V R) := by
162     ext i j
163     by_cases hij : i = j <;>
164       simp [transfer, RingHom.mapMatrix_apply, Matrix.map_apply,
165         Polynomial.constantCoeff_apply, adjacency_coeff_zero, Matrix.one_apply, hij]
166   rw [h, Matrix.det_one]
167 
168 theorem denominator_mul_inverse :
169     (denominator G m : PowerSeries R) * denominatorInverse G m = 1 := by
170   apply PowerSeries.mul_invOfUnit
171   simpa [Polynomial.constantCoeff_coe] using denominator_coeff_zero G m
172 
173 theorem denominator_inverse_mul :
174     denominatorInverse G m * (denominator G m : PowerSeries R) = 1 := by
175   apply PowerSeries.invOfUnit_mul
176   simpa [Polynomial.constantCoeff_coe] using denominator_coeff_zero G m
177 
178 theorem transfer_mul_seriesMatrix :
179     Polynomial.coeToPowerSeries.ringHom.mapMatrix (transfer G m) * seriesMatrix G m = 1 := by
180   have ht : Polynomial.coeToPowerSeries.ringHom.mapMatrix (transfer G m) =
181       1 - adjacencySeries G m := by
182     rw [transfer, adjacencySeries, map_sub, map_one]
183   rw [ht, sub_mul, one_mul]
184   exact sub_eq_iff_eq_add.mpr (seriesMatrix_eq_one_add_adjacency_mul G m)
185 
186 theorem seriesMatrix_eq_rationalMatrix : seriesMatrix G m =
187     ReleaseTransferMatrix.rationalMatrix Polynomial.coeToPowerSeries.ringHom
188       (transfer G m) (denominatorInverse G m) := by
189   let Z := ReleaseTransferMatrix.rationalMatrix Polynomial.coeToPowerSeries.ringHom
190     (transfer G m) (denominatorInverse G m)
191   have hleft : Z * Polynomial.coeToPowerSeries.ringHom.mapMatrix (transfer G m) = 1 :=
192     ReleaseTransferMatrix.rationalMatrix_mul _ _ _ (denominator_inverse_mul G m)
193   calc
194     seriesMatrix G m = 1 * seriesMatrix G m := (one_mul _).symm
195     _ = (Z * Polynomial.coeToPowerSeries.ringHom.mapMatrix (transfer G m)) *
196       seriesMatrix G m := by rw [hleft]
197     _ = Z * (Polynomial.coeToPowerSeries.ringHom.mapMatrix (transfer G m) *
198       seriesMatrix G m) := mul_assoc _ _ _
199     _ = Z := by rw [transfer_mul_seriesMatrix, mul_one]
200 
201 theorem denominator_mul_series (s t : V) :
202     (denominator G m : PowerSeries R) * series G m s t =
203       (Matrix.adjugate (transfer G m) s t : Polynomial R) := by
204   have h := ReleaseTransferMatrix.denominator_smul_rationalMatrix
205     Polynomial.coeToPowerSeries.ringHom (transfer G m) (denominatorInverse G m)
206     (denominator_mul_inverse G m)
207   rw [← seriesMatrix_eq_rationalMatrix] at h
208   exact congrFun (congrFun h s) t
209 
210 noncomputable def endpointSeries (u v : V → R) : PowerSeries R :=
211   ReleaseTransferMatrix.contract (PowerSeries.C ∘ u) (seriesMatrix G m) (PowerSeries.C ∘ v)
212 
213 noncomputable def endpointNumerator (u v : V → R) : Polynomial R :=
214   ReleaseTransferMatrix.contract (Polynomial.C ∘ u) (Matrix.adjugate (transfer G m))
215     (Polynomial.C ∘ v)
216 
217 theorem endpoint_rationality (u v : V → R) :
218     (denominator G m : PowerSeries R) * endpointSeries G m u v =
219       (endpointNumerator G m u v : PowerSeries R) := by
220   rw [endpointSeries, seriesMatrix_eq_rationalMatrix]
221   simpa [endpointNumerator, denominator, Function.comp_def] using
222     ReleaseTransferMatrix.rational_endpoint_identity Polynomial.coeToPowerSeries.ringHom
223       (transfer G m) (denominatorInverse G m) (denominator_mul_inverse G m)
224       (Polynomial.C ∘ u) (Polynomial.C ∘ v)
225 
226 theorem endpoint_coeff (u v : V → R) (n : ℕ) :
227     PowerSeries.coeff n (endpointSeries G m u v) =
228       ∑ i, ∑ j, u i * coefficient G m i j n * v j := by
229   simp [endpointSeries, ReleaseTransferMatrix.contract, seriesMatrix,
230     map_sum, PowerSeries.coeff_C_mul, PowerSeries.coeff_mul_C]
231 
232 theorem endpoint_recurrence_at_zero_coefficient (u v : V → R) (n : ℕ)
233     (h : (endpointNumerator G m u v).coeff n = 0) :
234     ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n,
235       (denominator G m).coeff p.1 * PowerSeries.coeff p.2 (endpointSeries G m u v) = 0 := by
236   have hc := congrArg (PowerSeries.coeff n) (endpoint_rationality G m u v)
237   rw [PowerSeries.coeff_mul] at hc
238   simpa [h] using hc
239 
240 theorem endpoint_recurrence (u v : V → R) (n : ℕ)
241     (h : (endpointNumerator G m u v).degree < (n : WithBot ℕ)) :
242     ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n,
243       (denominator G m).coeff p.1 * PowerSeries.coeff p.2 (endpointSeries G m u v) = 0 := by
244   exact endpoint_recurrence_at_zero_coefficient G m u v n
245     (Polynomial.coeff_eq_zero_of_degree_lt h)
246 
247 end Komorebi.PaperII.ReleaseTransferScalar

Back to source controls