CompanionCompletion.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.CompanionBridge
6 import KomorebiPaperIV.Wronskians
7 
8 /-! # Complete companion entry and determinant bridges
9 
10 The matrix exponential is identified with the transpose of the actual
11 derivative matrix. Its determinant is then obtained from the proved Wronskian,
12 without assuming a determinant-of-exponential formula.
13 -/
14 
15 namespace Komorebi.PaperIV
16 open scoped PowerSeries
17 noncomputable section
18 
19 /-- Taylor expansion of every derivative of a finite exponential sum. -/
20 theorem hasSum_exponentialSumJet (N : ℕ) (w a : ℕ → ℂ) (k : ℕ) (z : ℂ) :
21     HasSum (fun m => (m.factorial : ℂ)⁻¹ *
22       exponentialSumJet N w a (m + k) 0 * z ^ m)
23       (exponentialSumJet N w a k z) := by
24   have h := hasSum_sum (s := Finset.range N) (fun l _ =>
25     (NormedSpace.expSeries_div_hasSum_exp (a l * z)).mul_left (w l * a l ^ k))
26   rw [← Complex.exp_eq_exp_ℂ] at h
27   apply h.congr_fun
28   intro m
29   simp only [exponentialSumJet, mul_zero, Complex.exp_zero, mul_one,
30     Finset.mul_sum, Finset.sum_mul, pow_add, mul_pow, div_eq_mul_inv]
31   apply Finset.sum_congr rfl
32   intro l _
33   ring
34 
35 /-- All Taylor coefficients of a signed section's analytic derivatives. -/
36 theorem entireSigned_derivative_at_zero {N j : ℕ} (hN : 0 < N) (hj : j < N)
37     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
38     (k : ℕ) :
39     deriv^[k] (entireSigned N j omega rho) 0 =
40       (k.factorial : ℂ) * PowerSeries.coeff k (signedSection (R := ℂ) N j) := by
41   rw [entireSigned_derivative_eq_scaled_transfer,
42     entireTransfer_derivative_at_zero hN hj homega,
43     signedSection_eq_inv_pow_mul_transferSection hN hj hrho,
44     PowerSeries.coeff_C_mul]
45   ring
46 
47 /-- Convergent derivative series, with the manuscript's factorial scaling. -/
48 theorem hasSum_entireSigned_derivative {N j : ℕ} (hN : 0 < N) (hj : j < N)
49     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
50     (k : ℕ) (z : ℂ) :
51     HasSum (fun m => (m.factorial : ℂ)⁻¹ * ((m + k).factorial : ℂ) *
52       PowerSeries.coeff (m + k) (signedSection (R := ℂ) N j) * z ^ m)
53       (deriv^[k] (entireSigned N j omega rho) z) := by
54   have h := hasSum_exponentialSumJet N
55     (fun l => (rho ^ j)⁻¹ * (N : ℂ)⁻¹ * ((omega ^ j)⁻¹) ^ l)
56     (fun l => rho * omega ^ l) k z
57   rw [entireSigned_eq_exponentialSum, iteratedDeriv_exponentialSum]
58   apply h.congr_fun
59   intro m
60   have hd := entireSigned_derivative_at_zero hN hj homega hrho (m + k)
61   rw [entireSigned_eq_exponentialSum, iteratedDeriv_exponentialSum] at hd
62   rw [hd]
63   ring
64 
65 /-- Each matrix entry is an actual derivative, not a formal series symbol. -/
66 theorem signedFundamentalMatrix_entry_eq_derivative {N : ℕ} (hN : 0 < N)
67     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
68     (z : ℂ) (p q : Fin N) :
69     signedFundamentalMatrix N z p q =
70       deriv^[q.val] (entireSigned N p.val omega rho) z := by
71   apply (hasSum_signedFundamentalMatrix_entry N z p q).unique
72   convert hasSum_entireSigned_derivative hN p.isLt homega hrho q.val z using 1
73   funext m
74   rw [signedShiftMatrix_pow_apply N m hN, coeff_signedSection]
75   simp only [signedSectionCoeff, Nat.add_comm m q.val]
76   have hf : ((q.val + m).factorial : ℂ) ≠ 0 := by
77     exact_mod_cast (q.val + m).factorial_ne_zero
78   by_cases he : p.val = (q.val + m) % N
79   · simp only [he, ite_true, map_div₀, map_one, map_natCast]
80     field_simp
81   · simp [he, Ne.symm he]
82 
83 /-- The companion determinant is exactly one for every complex parameter. -/
84 theorem signedFundamentalMatrix_det {N : ℕ} (hN : 1 < N)
85     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
86     (z : ℂ) :
87     (signedFundamentalMatrix N z).det = 1 := by
88   have hm : signedFundamentalMatrix N z =
89       (Matrix.of (fun k j : Fin N =>
90         deriv^[k.val] (entireSigned N j.val omega rho) z)).transpose := by
91     ext p q
92     exact signedFundamentalMatrix_entry_eq_derivative (by omega) homega hrho z p q
93   rw [hm, Matrix.det_transpose]
94   exact signedWronskian_eq_one hN homega hrho z
95 
96 /-- The residue of the displacement from column q to row p. -/
97 def companionDisplacement {N : ℕ} (p q : Fin N) : ℕ :=
98   if q.val ≤ p.val then p.val - q.val else N + p.val - q.val
99 
100 theorem companionDisplacement_lt {N : ℕ} (p q : Fin N) :
101     companionDisplacement p q < N := by
102   unfold companionDisplacement
103   have hp := p.isLt
104   have hq := q.isLt
105   split_ifs <;> omega
106 
107 /-- Whether the displacement crosses the signed edge. -/
108 def companionEntrySign {N : ℕ} (p q : Fin N) : ℂ :=
109   if q.val ≤ p.val then 1 else -1
110 
111 /-- Closed packet form of every power entry, including its wraparound sign. -/
112 theorem signedShiftMatrix_pow_entry_packet {N : ℕ} (hN : 0 < N)
113     (p q : Fin N) (m : ℕ) :
114     (signedShiftMatrix (R := ℂ) N ^ m) p q =
115       companionEntrySign p q *
116         (if m % N = companionDisplacement p q then (-1 : ℂ) ^ (m / N) else 0) := by
117   rw [signedShiftMatrix_pow_apply N m hN]
118   have hp := p.isLt
119   have hq := q.isLt
120   have hm := Nat.mod_lt m hN
121   have hmod : (q.val + m) % N = (q.val + m % N) % N := by
122     simp only [Nat.add_mod, Nat.mod_mod]
123   have hdiv : (q.val + m) / N = (q.val + m % N) / N + m / N := by
124     conv_lhs => rw [← Nat.mod_add_div m N]
125     rw [← Nat.add_assoc, Nat.add_mul_div_left _ _ hN]
126   rw [hmod, hdiv]
127   unfold companionEntrySign companionDisplacement
128   by_cases hqp : q.val ≤ p.val
129   · simp only [ite_eq_left hqp, one_mul]
130     by_cases he : m % N = p.val - q.val
131     · have hsum : q.val + m % N = p.val := by omega
132       rw [hsum]
133       simp only [Nat.mod_eq_of_lt hp, Nat.div_eq_of_lt hp, ite_true, zero_add, he]
134     · have hne : p.val ≠ (q.val + m % N) % N := by
135         by_cases hs : q.val + m % N < N
136         · rw [Nat.mod_eq_of_lt hs]
137           omega
138         · rw [Nat.mod_eq_sub_mod (by omega), Nat.mod_eq_of_lt (by omega)]
139           omega
140       simp only [ite_eq_right he, ite_eq_right hne]
141   · simp only [ite_eq_right hqp]
142     by_cases he : m % N = N + p.val - q.val
143     · have hsum : q.val + m % N = N + p.val := by omega
144       have hd : (N + p.val) / N = 1 := by
145         simpa [Nat.div_eq_of_lt hp, Nat.add_comm] using Nat.add_mul_div_left p.val 1 hN
146       rw [hsum]
147       simp only [Nat.add_mod_left, Nat.mod_eq_of_lt hp, ite_true, hd, he]
148       rw [pow_add]
149       simp
150     · have hne : p.val ≠ (q.val + m % N) % N := by
151         by_cases hs : q.val + m % N < N
152         · rw [Nat.mod_eq_of_lt hs]
153           omega
154         · rw [Nat.mod_eq_sub_mod (by omega), Nat.mod_eq_of_lt (by omega)]
155           omega
156       simp only [ite_eq_right he, ite_eq_right hne, mul_zero]
157 
158 /-- Corollary 6.5: every entry of exp(z J) is the stated signed section. -/
159 theorem signedFundamentalMatrix_entry {N : ℕ} (hN : 0 < N)
160     {omega rho : ℂ} (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1)
161     (z : ℂ) (p q : Fin N) :
162     signedFundamentalMatrix N z p q =
163       companionEntrySign p q * entireSigned N (companionDisplacement p q) omega rho z := by
164   apply (hasSum_signedFundamentalMatrix_entry N z p q).unique
165   have hs := (hasSum_entireSigned hN (companionDisplacement_lt p q) homega hrho z).mul_left
166     (companionEntrySign p q)
167   apply hs.congr_fun
168   intro m
169   rw [signedShiftMatrix_pow_entry_packet hN, coeff_signedSection]
170   simp only [signedSectionCoeff, map_div₀, map_one, map_natCast]
171   split_ifs <;> ring
172 
173 end
174 end Komorebi.PaperIV

Back to source controls