Wronskians.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.EntireBridge
6 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
7 import Mathlib.Algebra.BigOperators.Intervals
8 
9 /-!
10 # Analytic Wronskians of the cyclic bases
11 
12 The determinant calculation factors the derivative matrix into a Vandermonde
13 matrix, a diagonal exponential matrix, and a constant weight matrix. It does
14 not assume Abel's identity or invertibility of the Vandermonde matrix.
15 -/
16 
17 namespace Komorebi.PaperIV
18 noncomputable section
19 
20 /-- Derivative matrix for N finite exponential sums. -/
21 def exponentialJetMatrix (N : ℕ) (w : ℕ → Fin N → ℂ) (a : ℕ → ℂ) (z : ℂ) :
22     Matrix (Fin N) (Fin N) ℂ :=
23   fun k j => exponentialSumJet N (fun l => w l j) a k.val z
24 
25 theorem exponentialJetMatrix_factor (N : ℕ) (w : ℕ → Fin N → ℂ)
26     (a : ℕ → ℂ) (z : ℂ) :
27     exponentialJetMatrix N w a z =
28       Matrix.of (fun k l : Fin N => a l.val ^ k.val) *
29         Matrix.diagonal (fun l : Fin N => Complex.exp (a l.val * z)) *
30         Matrix.of (fun l j : Fin N => w l.val j) := by
31   ext k j
32   change (∑ l ∈ Finset.range N, w l j * a l ^ k.val * Complex.exp (a l * z)) = _
33   rw [Matrix.mul_apply]
34   simp only [Matrix.mul_diagonal, Matrix.of_apply]
35   rw [Finset.sum_range (fun l => w l j * a l ^ k.val * Complex.exp (a l * z))]
36   apply Finset.sum_congr rfl
37   intro l _
38   ring
39 
40 theorem det_exponentialJetMatrix (N : ℕ) (w : ℕ → Fin N → ℂ)
41     (a : ℕ → ℂ) (z : ℂ) :
42     (exponentialJetMatrix N w a z).det =
43       Complex.exp ((∑ l ∈ Finset.range N, a l) * z) *
44         (exponentialJetMatrix N w a 0).det := by
45   rw [exponentialJetMatrix_factor, exponentialJetMatrix_factor]
46   simp only [mul_zero, Complex.exp_zero, Matrix.diagonal_one,
47     Matrix.mul_one, Matrix.det_mul, Matrix.det_diagonal]
48   rw [← Complex.exp_sum, Finset.sum_range a, Finset.sum_mul]
49   ring
50 
51 theorem det_exponentialJetMatrix_constant (N : ℕ) (w : ℕ → Fin N → ℂ)
52     (a : ℕ → ℂ) (ha : ∑ l ∈ Finset.range N, a l = 0) (z : ℂ) :
53     (exponentialJetMatrix N w a z).det = (exponentialJetMatrix N w a 0).det := by
54   rw [det_exponentialJetMatrix, ha]
55   simp
56 
57 /-- The ordinary analytic Wronskian, using actual iterated derivatives. -/
58 def analyticWronskian {N : ℕ} (f : Fin N → ℂ → ℂ) (z : ℂ) : ℂ :=
59   Matrix.det (fun k j : Fin N => deriv^[k.val] (f j) z)
60 
61 theorem transferWronskian_constant {N : ℕ} (hN : 1 < N) {omega : ℂ}
62     (homega : IsPrimitiveRoot omega N) (lambda z : ℂ) :
63     analyticWronskian (fun j : Fin N => entireTransfer N j.val omega lambda) z =
64       analyticWronskian (fun j : Fin N => entireTransfer N j.val omega lambda) 0 := by
65   simp only [analyticWronskian, entireTransfer_eq_exponentialSum,
66     iteratedDeriv_exponentialSum]
67   apply det_exponentialJetMatrix_constant N
68     (fun l j => (N : ℂ)⁻¹ * ((omega ^ j.val)⁻¹) ^ l)
69     (fun l => lambda * omega ^ l)
70   rw [← Finset.mul_sum, homega.geom_sum_eq_zero hN, mul_zero]
71 
72 /-- Corollary 4.3, including its exact exponent and ordered basis. -/
73 theorem transferWronskian_eq {N : ℕ} (hN : 1 < N) {omega : ℂ}
74     (homega : IsPrimitiveRoot omega N) (lambda z : ℂ) :
75     analyticWronskian (fun j : Fin N => entireTransfer N j.val omega lambda) z =
76       lambda ^ (N * (N - 1) / 2) := by
77   rw [transferWronskian_constant hN homega]
78   have hm : (fun k j : Fin N => deriv^[k.val]
79       (entireTransfer N j.val omega lambda) 0) =
80       Matrix.diagonal (fun j : Fin N => lambda ^ j.val) := by
81     ext k j
82     rw [entireTransfer_initial_data (by omega) j.isLt k.isLt homega]
83     by_cases h : k = j
84     · subst k
85       simp
86     · simp [h, Fin.ext_iff.mpr.mt h]
87   rw [analyticWronskian, hm, Matrix.det_diagonal, Finset.prod_pow_eq_pow_sum]
88   rw [← Finset.sum_range (fun i => i), Finset.sum_range_id]
89 
90 theorem signedWronskian_constant {N : ℕ} (hN : 1 < N) {omega : ℂ}
91     (homega : IsPrimitiveRoot omega N) (rho z : ℂ) :
92     analyticWronskian (fun j : Fin N => entireSigned N j.val omega rho) z =
93       analyticWronskian (fun j : Fin N => entireSigned N j.val omega rho) 0 := by
94   simp only [analyticWronskian, entireSigned_eq_exponentialSum,
95     iteratedDeriv_exponentialSum]
96   apply det_exponentialJetMatrix_constant N
97     (fun l j => (rho ^ j.val)⁻¹ * (N : ℂ)⁻¹ * ((omega ^ j.val)⁻¹) ^ l)
98     (fun l => rho * omega ^ l)
99   rw [← Finset.mul_sum, homega.geom_sum_eq_zero hN, mul_zero]
100 
101 /-- Corollary 5.4: the signed analytic Wronskian is identically one. -/
102 theorem signedWronskian_eq_one {N : ℕ} (hN : 1 < N) {omega rho : ℂ}
103     (homega : IsPrimitiveRoot omega N) (hrho : rho ^ N = -1) (z : ℂ) :
104     analyticWronskian (fun j : Fin N => entireSigned N j.val omega rho) z = 1 := by
105   rw [signedWronskian_constant hN homega]
106   have hm : (fun k j : Fin N => deriv^[k.val]
107       (entireSigned N j.val omega rho) 0) = (1 : Matrix (Fin N) (Fin N) ℂ) := by
108     ext k j
109     rw [entireSigned_initial_data (by omega) j.isLt k.isLt homega hrho]
110     simp [Matrix.one_apply, Fin.ext_iff]
111   rw [analyticWronskian, hm, Matrix.det_one]
112 
113 end
114 end Komorebi.PaperIV

Back to source controls