ReleaseTransferConsequences.lean

1 import KomorebiVerification.PaperII.ReleaseTransferMultigradedRational
2 import Mathlib.FieldTheory.RatFunc.Basic
3 
4 /-! Consequences of the semantic transfer identities. Coefficient recurrences
5 use the actual vanishing coefficient, so the zero numerator at index zero is
6 included. Over a field the reduced rational-function denominator divides the
7 transfer determinant. -/
8 set_option autoImplicit false
9 open scoped BigOperators
10 
11 namespace Komorebi.PaperII.ReleaseTransferConsequences
12 universe u v w z
13 
14 section Recurrence
15 variable {R : Type u} [CommRing R]
16 
17 theorem recurrence_of_coefficient_zero (P Q : Polynomial R) (Z : PowerSeries R)
18     (h : (Q : PowerSeries R) * Z = (P : PowerSeries R)) (n : ℕ)
19     (hn : P.coeff n = 0) :
20     ∑ k ∈ Finset.range (n + 1), Q.coeff k * PowerSeries.coeff (n - k) Z = 0 := by
21   have hc := congrArg (PowerSeries.coeff n) h
22   rw [PowerSeries.coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk] at hc
23   simpa [hn] using hc
24 
25 theorem recurrence_of_degree_lt (P Q : Polynomial R) (Z : PowerSeries R)
26     (h : (Q : PowerSeries R) * Z = (P : PowerSeries R)) (n : ℕ)
27     (hn : P.degree < (n : WithBot ℕ)) :
28     ∑ k ∈ Finset.range (n + 1), Q.coeff k * PowerSeries.coeff (n - k) Z = 0 :=
29   recurrence_of_coefficient_zero P Q Z h n (Polynomial.coeff_eq_zero_of_degree_lt hn)
30 
31 theorem zero_numerator_recurrence (Q : Polynomial R) (Z : PowerSeries R)
32     (h : (Q : PowerSeries R) * Z = 0) (n : ℕ) :
33     ∑ k ∈ Finset.range (n + 1), Q.coeff k * PowerSeries.coeff (n - k) Z = 0 := by
34   exact recurrence_of_coefficient_zero 0 Q Z (by simpa using h) n (by simp)
35 
36 end Recurrence
37 
38 section Scalar
39 open TransferZeta
40 variable {V : Type u} {E : Type v} {R : Type w}
41 variable [Fintype V] [Fintype E] [DecidableEq V] [CommRing R]
42 variable (G : PositiveWeightedMultigraph V E) (m : E → R)
43 
44  theorem scalar_denominator_ne_zero [Nontrivial R] :
45     ReleaseTransferScalar.denominator G m ≠ 0 := by
46   intro h
47   have hc := ReleaseTransferScalar.denominator_coeff_zero G m
48   rw [h, Polynomial.coeff_zero] at hc
49   exact zero_ne_one hc
50 
51  theorem scalar_endpoint_unique (u v : V → R) (Z : PowerSeries R)
52     (h : (ReleaseTransferScalar.denominator G m : PowerSeries R) * Z =
53       (ReleaseTransferScalar.endpointNumerator G m u v : PowerSeries R)) :
54     Z = ReleaseTransferScalar.endpointSeries G m u v := by
55   calc
56     Z = 1 * Z := (one_mul _).symm
57     _ = (ReleaseTransferScalar.denominatorInverse G m *
58       (ReleaseTransferScalar.denominator G m : PowerSeries R)) * Z := by
59         rw [ReleaseTransferScalar.denominator_inverse_mul]
60     _ = ReleaseTransferScalar.denominatorInverse G m *
61       ((ReleaseTransferScalar.denominator G m : PowerSeries R) * Z) := mul_assoc _ _ _
62     _ = ReleaseTransferScalar.denominatorInverse G m *
63       ((ReleaseTransferScalar.denominator G m : PowerSeries R) *
64         ReleaseTransferScalar.endpointSeries G m u v) := by
65           rw [h, ReleaseTransferScalar.endpoint_rationality]
66     _ = ReleaseTransferScalar.endpointSeries G m u v := by
67       rw [← mul_assoc, ReleaseTransferScalar.denominator_inverse_mul, one_mul]
68 
69 end Scalar
70 
71 section RationalFunction
72 open TransferZeta
73 variable {V : Type u} {E : Type v} {K : Type w}
74 variable [Fintype V] [Fintype E] [DecidableEq V] [Field K]
75 variable (G : PositiveWeightedMultigraph V E) (m : E → K)
76 
77 noncomputable def endpointRationalFunction (u v : V → K) : RatFunc K :=
78   algebraMap (Polynomial K) (RatFunc K) (ReleaseTransferScalar.endpointNumerator G m u v) /
79     algebraMap (Polynomial K) (RatFunc K) (ReleaseTransferScalar.denominator G m)
80 
81 theorem reduced_denominator_dvd (u v : V → K) :
82     RatFunc.denom (endpointRationalFunction G m u v) ∣ ReleaseTransferScalar.denominator G m :=
83   RatFunc.denom_div_dvd _ _
84 
85 end RationalFunction
86 
87 section Multigraded
88 variable {V : Type u} {E : Type v} {σ : Type w} {R : Type z}
89 variable [Fintype V] [Fintype E] [DecidableEq V] [DecidableEq σ] [CommRing R]
90 variable (G : ReleaseTransferMultigraded.Graph V E σ) (m : E → R)
91 
92 theorem multigraded_denominator_ne_zero [Nontrivial R] :
93     ReleaseTransferMultigraded.denominator G m ≠ 0 := by
94   intro h
95   have hc := ReleaseTransferMultigraded.denominator_constantCoeff G m
96   rw [h, map_zero] at hc
97   exact zero_ne_one hc
98 
99 theorem multigraded_endpoint_unique (u v : V → R) (Z : MvPowerSeries σ R)
100     (h : (ReleaseTransferMultigraded.denominator G m : MvPowerSeries σ R) * Z =
101       (ReleaseTransferMultigraded.endpointNumerator G m u v : MvPowerSeries σ R)) :
102     Z = ReleaseTransferMultigraded.endpointSeries G m u v := by
103   calc
104     Z = 1 * Z := (one_mul _).symm
105     _ = (ReleaseTransferMultigraded.denominatorInverse G m *
106       (ReleaseTransferMultigraded.denominator G m : MvPowerSeries σ R)) * Z := by
107         rw [ReleaseTransferMultigraded.denominator_inverse_mul]
108     _ = ReleaseTransferMultigraded.denominatorInverse G m *
109       ((ReleaseTransferMultigraded.denominator G m : MvPowerSeries σ R) * Z) := mul_assoc _ _ _
110     _ = ReleaseTransferMultigraded.denominatorInverse G m *
111       ((ReleaseTransferMultigraded.denominator G m : MvPowerSeries σ R) *
112         ReleaseTransferMultigraded.endpointSeries G m u v) := by
113           rw [h, ReleaseTransferMultigraded.endpoint_rationality]
114     _ = ReleaseTransferMultigraded.endpointSeries G m u v := by
115       rw [← mul_assoc, ReleaseTransferMultigraded.denominator_inverse_mul, one_mul]
116 
117 end Multigraded
118 end Komorebi.PaperII.ReleaseTransferConsequences

Back to source controls