DiagonalFredholm.lean

1 /-
2 Copyright (c) 2026 Komorebi P. All rights reserved.
3 Authors: Komorebi P.
4 -/
5 import KomorebiPaperIV.DiagonalTrace
6 import KomorebiPaperIV.InfiniteSymmetric
7 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
8 
9 namespace Komorebi.PaperIV
10 noncomputable section
11 open Set Filter InnerProductSpace
12 open scoped Topology Classical InnerProductSpace
13 
14 def diagonalCompression {ι : Type} (a : ι → ℂ) (S : Finset ι) : Matrix S S ℂ :=
15   fun i j => ⟪diagonalHilbertBasis ι i.val, diagonalOperator a (diagonalHilbertBasis ι j.val)⟫_ℂ
16 
17 theorem diagonalCompression_eq_diagonal {ι : Type} {a : ι → ℂ}
18     (ha : Summable (fun i => ‖a i‖)) (S : Finset ι) :
19     diagonalCompression a S = Matrix.diagonal (fun i : S => a i.val) := by
20   ext i j
21   simp only [diagonalCompression, diagonalHilbertBasis_inner, diagonalOperator_apply ha,
22     diagonalHilbertBasis_apply, Matrix.diagonal_apply]
23   by_cases h : i = j
24   · simp [h]
25   · have hv : i.val ≠ j.val := fun he => h (Subtype.ext he)
26     simp [h, hv]
27 
28 theorem diagonalCompression_determinant {ι : Type} {a : ι → ℂ}
29     (ha : Summable (fun i => ‖a i‖)) (S : Finset ι) (w : ℂ) :
30     Matrix.det (1 - w • diagonalCompression a S) = ∏ i ∈ S, (1 - w * a i) := by
31   have he : (1 - w • diagonalCompression a S) = Matrix.diagonal (fun i : S => 1 - w * a i.val) := by
32     rw [diagonalCompression_eq_diagonal ha]
33     ext i j
34     by_cases h : i = j <;> simp [h]
35   rw [he, Matrix.det_diagonal]
36   exact Finset.prod_coe_sort S (fun i => 1 - w * a i)
37 
38 /-- Specialized diagonal Fredholm determinant, obtained as a limit of the
39 actual finite-compression determinants in the next theorem. -/
40 def diagonalFredholmDeterminant {ι : Type} (a : ι → ℂ) (w : ℂ) : ℂ := ∏' i, (1 - w * a i)
41 
42 theorem diagonalFredholmDeterminant_compression_limit {ι : Type} {a : ι → ℂ}
43     (ha : Summable (fun i => ‖a i‖)) (w : ℂ) :
44     Tendsto (fun S : Finset ι => Matrix.det (1 - w • diagonalCompression a S)) atTop
45       (𝓝 (diagonalFredholmDeterminant a w)) := by
46   have hm : Summable (fun i => ‖w * a i‖) := by simpa only [norm_mul] using ha.mul_left ‖w‖
47   simpa only [diagonalCompression_determinant ha, diagonalFredholmDeterminant] using!
48     (multipliable_one_sub_of_summable hm).hasProd
49 
50 def reducedZeroEigenvalue (N : ℕ) (i : ZeroMultiplicityIndex (entireReducedDenominator N)) : ℂ :=
51   (indexedZero i)⁻¹
52 
53 theorem reducedZeroEigenvalue_norm_summable {N : ℕ} (hN : 2 ≤ N) :
54     Summable (fun i => ‖reducedZeroEigenvalue N i‖) := by
55   simpa [reducedZeroEigenvalue, norm_inv, one_div] using zeroMultiplicity_reciprocal_summable
56     (entireReducedDenominator_reciprocal_zeros_summable hN)
57 
58 def reducedZeroOperator (N : ℕ) := diagonalOperator (reducedZeroEigenvalue N)
59 
60 theorem reducedZeroOperator_traceClass {N : ℕ} (hN : 2 ≤ N) :
61     IsHilbertTraceClass (reducedZeroOperator N) :=
62   diagonalOperator_traceClass (reducedZeroEigenvalue_norm_summable hN)
63 
64 theorem reducedZeroOperator_basis {N : ℕ} (hN : 2 ≤ N)
65     (i : ZeroMultiplicityIndex (entireReducedDenominator N)) :
66     reducedZeroOperator N (diagonalHilbertBasis _ i) =
67       (indexedZero i)⁻¹ • diagonalHilbertBasis _ i :=
68   diagonalOperator_apply_basis (reducedZeroEigenvalue_norm_summable hN) i
69 
70 theorem reducedZeroOperator_fredholm {N : ℕ} (hN : 2 ≤ N) (w : ℂ) :
71     diagonalFredholmDeterminant (reducedZeroEigenvalue N) w = entireReducedDenominator N w := by
72   calc
73     _ = fullCanonicalProduct (entireReducedDenominator N) w := by
74       simp only [diagonalFredholmDeterminant, reducedZeroEigenvalue, fullCanonicalProduct, div_eq_mul_inv]
75     _ = _ := congrFun (entireReducedDenominator_eq_fullCanonicalProduct hN).symm w
76 
77 theorem reducedZeroOperator_trace_power {N m : ℕ} (hN : 2 ≤ N) (hm : 0 < m)
78     {κ : Type} (b : HilbertBasis κ ℂ (lp (fun _ : ZeroMultiplicityIndex (entireReducedDenominator N) => ℂ) 2)) :
79     hilbertBasisTrace b (reducedZeroOperator N ^ m) = kappaCoeff (R := ℂ) N m := by
80   rw [reducedZeroOperator, diagonalOperator_pow_trace (reducedZeroEigenvalue_norm_summable hN) m
81     (summable_norm_positive_powers (reducedZeroEigenvalue_norm_summable hN) hm),
82     kappaCoeff_eq_zeroPowerSum hN hm]
83   simp [reducedZeroEigenvalue, zeroPowerSum, one_div, inv_pow]
84 
85 /-- The actual compression determinants converge uniformly on every compact
86 set to the manuscript's entire denominator. -/
87 theorem reducedZeroOperator_finite_determinants_uniform {N : ℕ} (hN : 2 ≤ N)
88     {K : Set ℂ} (hK : IsCompact K) :
89     TendstoUniformlyOn
90       (fun S : Finset (ZeroMultiplicityIndex (entireReducedDenominator N)) =>
91         fun w => Matrix.det (1 - w • diagonalCompression (reducedZeroEigenvalue N) S))
92       (entireReducedDenominator N) atTop K := by
93   have h := (entireReducedDenominator_hadamard_uniform hN hK).tendstoUniformlyOn
94   simpa only [diagonalCompression_determinant (reducedZeroEigenvalue_norm_summable hN),
95     reducedZeroEigenvalue, div_eq_mul_inv, Finset.prod_fn] using h
96 
97 end
98 end Komorebi.PaperIV

Back to source controls