SpectralCertificates.lean

1 import KomorebiVerification.SingleOperatorGraph
2 import Mathlib.Analysis.InnerProductSpace.Spectrum
3 import Mathlib.Analysis.Matrix.Hermitian
4 
5 /-!
6 # Internally constructed spectral certificates for Paper I
7 
8 The old graph theorem takes a multiplicity-grouped eigenbasis as an input.
9 This extension first groups any finite eigenbasis by equality of eigenvalues,
10 then obtains that basis from the finite-dimensional spectral theorem.  The
11 public self-adjoint theorem takes no eigenbasis, extraction polynomial,
12 quotient map, multiplicity function, or maximizer as an input.
13 -/
14 
15 set_option autoImplicit false
16 
17 noncomputable section
18 
19 namespace Komorebi.PaperICompletion.SpectralCertificates
20 
21 open Komorebi.SingleOperatorGraph
22 open scoped BigOperators
23 
24 universe u v w
25 
26 section Grouping
27 variable {k : Type u} [Field k] {I : Type v} [Fintype I]
28 variable {V : Type w} [AddCommGroup V] [Module k V]
29 
30 /-- The distinct eigenvalue labels of a finite indexed eigenvalue list. -/
31 def EigenLabels (μ : I → k) := Set.range μ
32 
33 noncomputable instance eigenLabelsFintype (μ : I → k) : Fintype (EigenLabels μ) :=
34   (Set.finite_range μ).fintype
35 
36 /-- The actual number of entries of the list equal to a specified scalar. -/
37 def eigenMultiplicity (μ : I → k) (value : k) : ℕ := Nat.card {i : I // μ i = value}
38 
39 /-- A finite coordinate system for one eigenvalue fibre. -/
40 def eigenFibreEquiv (μ : I → k) (value : k) :
41     {i : I // μ i = value} ≃ Fin (eigenMultiplicity μ value) := by
42   classical
43   exact Fintype.equivFinOfCardEq (by simp [eigenMultiplicity, Nat.card_eq_fintype_card])
44 
45 /-- Re-index the whole basis by distinct eigenvalues and their multiplicities. -/
46 def groupedIndexEquiv (μ : I → k) :
47     (Σ value : EigenLabels μ, Fin (eigenMultiplicity μ value.val)) ≃ I :=
48   (Equiv.sigmaCongrRight fun value : EigenLabels μ ↦ (eigenFibreEquiv μ value.val).symm).trans
49     (Equiv.sigmaSubtypeFiberEquiv μ (fun value ↦ value ∈ Set.range μ)
50       (fun i ↦ Set.mem_range_self i))
51 
52 omit [Field k] in
53 theorem groupedIndex_eigenvalue (μ : I → k)
54     (z : Σ value : EigenLabels μ, Fin (eigenMultiplicity μ value.val)) :
55     μ (groupedIndexEquiv μ z) = z.1.val := by
56   change μ ((eigenFibreEquiv μ z.1.val).symm z.2).val = z.1.val
57   exact ((eigenFibreEquiv μ z.1.val).symm z.2).property
58 
59 /-- The multiplicity-grouped basis, constructed rather than supplied. -/
60 def groupedEigenbasis (μ : I → k) (b : Module.Basis I k V) :
61     Module.Basis (Σ value : EigenLabels μ, Fin (eigenMultiplicity μ value.val)) k V :=
62   b.reindex (groupedIndexEquiv μ).symm
63 
64 theorem groupedEigenbasis_is_eigenbasis (T : Module.End k V)
65     (μ : I → k) (b : Module.Basis I k V)
66     (hEigen : ∀ i, T (b i) = μ i • b i)
67     (z : Σ value : EigenLabels μ, Fin (eigenMultiplicity μ value.val)) :
68     T (groupedEigenbasis μ b z) = z.1.val • groupedEigenbasis μ b z := by
69   simp only [groupedEigenbasis, Module.Basis.reindex_apply, Equiv.symm_symm]
70   rw [hEigen, groupedIndex_eigenvalue μ z]
71 
72 /-- Maximum repeated-eigenvalue count, with the empty-list value fixed at zero. -/
73 def maxEigenMultiplicity (μ : I → k) : ℕ :=
74   Finset.univ.sup fun value : EigenLabels μ ↦ eigenMultiplicity μ value.val
75 
76 omit [Field k] in
77 theorem eigenMultiplicity_le_max (μ : I → k) (value : EigenLabels μ) :
78     eigenMultiplicity μ value.val ≤ maxEigenMultiplicity μ := by
79   unfold maxEigenMultiplicity
80   exact Finset.le_sup (f := fun z : EigenLabels μ ↦ eigenMultiplicity μ z.val)
81     (Finset.mem_univ value)
82 
83 /-- Distinct labels, grouped basis, projectors, and maximizer are all built internally. -/
84 theorem seedNumber_isLeast_of_eigenbasis [Nonempty I]
85     (T : Module.End k V) (μ : I → k) (b : Module.Basis I k V)
86     (hEigen : ∀ i, T (b i) = μ i • b i) :
87     IsLeast {r : ℕ | SeedNumberLE T r} (maxEigenMultiplicity μ) := by
88   classical
89   let i : I := Classical.arbitrary I
90   have hnonempty : (Finset.univ : Finset (EigenLabels μ)).Nonempty :=
91     ⟨⟨μ i, Set.mem_range_self i⟩, Finset.mem_univ _⟩
92   obtain ⟨value, _hvalue, hmax⟩ := Finset.exists_mem_eq_sup Finset.univ hnonempty
93     (fun value : EigenLabels μ ↦ eigenMultiplicity μ value.val)
94   exact diagonalizable_seedNumber_isLeast_of_distinct_eigenvalues T
95     (maxEigenMultiplicity μ) (fun value : EigenLabels μ ↦ eigenMultiplicity μ value.val)
96     Subtype.val (groupedEigenbasis μ b)
97     (groupedEigenbasis_is_eigenbasis T μ b hEigen) Subtype.val_injective
98     (eigenMultiplicity_le_max μ) value hmax.symm
99 
100 end Grouping
101 
102 section SelfAdjoint
103 variable {𝕜 : Type u} [RCLike 𝕜]
104 variable {V : Type v} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V]
105 variable [FiniteDimensional 𝕜 V]
106 
107 /-- The list supplied by the proven finite-dimensional spectral theorem. -/
108 def spectralList (T : Module.End 𝕜 V) (hT : T.IsSymmetric) :
109     Fin (Module.finrank 𝕜 V) → 𝕜 :=
110   fun i ↦ (hT.eigenvalues rfl i : 𝕜)
111 
112 /-- Multiplicities here are intrinsic eigenspace dimensions, not abstract input numbers. -/
113 theorem spectralList_multiplicity_eq_finrank
114     (T : Module.End 𝕜 V) (hT : T.IsSymmetric) (value : 𝕜) :
115     eigenMultiplicity (spectralList T hT) value =
116       Module.finrank 𝕜 (Module.End.eigenspace T value) := by
117   classical
118   simpa [eigenMultiplicity, Nat.card_eq_fintype_card, Fintype.card_subtype, spectralList]
119     using hT.card_filter_eigenvalues_eq rfl value
120 
121 /-- Exact seed number from self-adjointness alone, including the zero space. -/
122 theorem selfAdjoint_seedNumber_isLeast
123     (T : Module.End 𝕜 V) (hT : T.IsSymmetric) :
124     IsLeast {r : ℕ | SeedNumberLE T r}
125       (maxEigenMultiplicity (spectralList T hT)) := by
126   classical
127   by_cases hdim : Module.finrank 𝕜 V = 0
128   · let : Subsingleton V := (Module.finrank_zero_iff).mp hdim
129     have hmax : maxEigenMultiplicity (spectralList T hT) = 0 := by
130       apply Finset.sup_eq_zero.mpr
131       intro value _
132       obtain ⟨i, _hi⟩ := value.property
133       exact False.elim (by have := i.isLt; omega)
134     rw [hmax]
135     exact seedNumber_zero_isLeast_of_subsingleton T
136   · let : NeZero (Module.finrank 𝕜 V) := ⟨hdim⟩
137     exact seedNumber_isLeast_of_eigenbasis T (spectralList T hT)
138       (hT.eigenvectorBasis rfl).toBasis (hT.apply_eigenvectorBasis rfl)
139 
140 /-- The result concerns the actual image algebra generated by the operator. -/
141 theorem selfAdjoint_operatorAlgebra_seedRanks
142     (T : Module.End 𝕜 V) (hT : T.IsSymmetric) :
143     Komorebi.SeedRankBasics.seedFinrank (operatorAlgebra T) V =
144         maxEigenMultiplicity (spectralList T hT) ∧
145       Komorebi.SeedRankBasics.seedRank (operatorAlgebra T) V =
146         (maxEigenMultiplicity (spectralList T hT) : Cardinal) := by
147   have h := selfAdjoint_seedNumber_isLeast T hT
148   exact ⟨operatorAlgebra_seedFinrank_eq_of_seedNumber_isLeast T _ h,
149     operatorAlgebra_seedRank_eq_of_seedNumber_isLeast T _ h⟩
150 
151 /-- The formula is a maximum of intrinsic eigenspace dimensions. -/
152 theorem selfAdjoint_seedRank_eq_max_eigenspace_finrank
153     (T : Module.End 𝕜 V) (hT : T.IsSymmetric) :
154     Komorebi.SeedRankBasics.seedRank (operatorAlgebra T) V =
155       (((Finset.univ.sup fun value : EigenLabels (spectralList T hT) ↦
156         Module.finrank 𝕜 (Module.End.eigenspace T value.val)) : ℕ) : Cardinal) := by
157   rw [(selfAdjoint_operatorAlgebra_seedRanks T hT).2]
158   simp only [maxEigenMultiplicity, spectralList_multiplicity_eq_finrank]
159 
160 end SelfAdjoint
161 
162 section Matrix
163 variable {𝕜 : Type u} [RCLike 𝕜] {n : Type v} [Fintype n] [DecidableEq n]
164 
165 /-- A Hermitian matrix needs no caller-supplied spectral certificate. -/
166 theorem hermitian_matrix_seedNumber_isLeast
167     (A : Matrix n n 𝕜) (hA : A.IsHermitian) :
168     IsLeast {r : ℕ | SeedNumberLE A.toEuclideanLin r}
169       (maxEigenMultiplicity (spectralList A.toEuclideanLin
170         (Matrix.isSymmetric_toEuclideanLin_iff.mpr hA))) :=
171   selfAdjoint_seedNumber_isLeast A.toEuclideanLin
172     (Matrix.isSymmetric_toEuclideanLin_iff.mpr hA)
173 
174 /-- In the real case, ordinary matrix symmetry is the sufficient input. -/
175 theorem real_symmetric_matrix_seedNumber_isLeast
176     (A : Matrix n n ℝ) (hA : A.IsSymm) :
177     IsLeast {r : ℕ | SeedNumberLE A.toEuclideanLin r}
178       (maxEigenMultiplicity (spectralList A.toEuclideanLin
179         (Matrix.isSymmetric_toEuclideanLin_iff.mpr
180           (Matrix.isHermitian_iff_isSymm.mpr hA)))) :=
181   hermitian_matrix_seedNumber_isLeast A (Matrix.isHermitian_iff_isSymm.mpr hA)
182 
183 end Matrix
184 end Komorebi.PaperICompletion.SpectralCertificates

Back to source controls