SpectralProjectors.lean

1 import Mathlib.LinearAlgebra.Eigenspace.Minpoly
2 import Mathlib.LinearAlgebra.Eigenspace.Semisimple
3 import Mathlib.LinearAlgebra.Trace
4 import Mathlib.Tactic
5 
6 /-! Actual Lagrange spectral projectors. Diagonalizability is the spanning of
7 actual eigenspaces. No eigenbasis or desired projector is assumed supplied. -/
8 set_option autoImplicit false
9 noncomputable section
10 namespace PaperX.SpectralProjectors
11 
12 open scoped BigOperators Polynomial
13 open Polynomial LinearMap Module.End
14 attribute [local instance] Classical.propDecidable
15 universe u v
16 variable {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V]
17 
18 /-- Exact finite-spectrum Lagrange selector; absent targets select zero. -/
19 def selector (s : Finset K) (a : K) : K[X] := by
20   classical
21   exact if a ∈ s then ∏ b ∈ s.erase a, C ((a-b)⁻¹) * (X-C b) else 0
22 
23 theorem selector_eval_self (s : Finset K) {a : K} (ha : a ∈ s) :
24     (selector s a).eval a = 1 := by
25   classical
26   simp only [selector, ite_eq_left ha, eval_prod, eval_mul, eval_C, eval_sub, eval_X]
27   apply Finset.prod_eq_one
28   intro b hb
29   exact inv_mul_cancel₀ (sub_ne_zero.mpr (Finset.ne_of_mem_erase hb).symm)
30 
31 theorem selector_eval_other (s : Finset K) {a b : K} (hb : b ∈ s) (hne : b ≠ a) :
32     (selector s a).eval b = 0 := by
33   classical
34   by_cases ha : a ∈ s
35   · simp only [selector, ite_eq_left ha, eval_prod, eval_mul, eval_C, eval_sub, eval_X]
36     exact Finset.prod_eq_zero (Finset.mem_erase.mpr ⟨hne, hb⟩) (by simp)
37   · simp [selector, ha]
38 
39 theorem selector_eval (s : Finset K) {a b : K} (hb : b ∈ s) :
40     (selector s a).eval b = if b = a then 1 else 0 := by
41   classical
42   by_cases h : b = a
43   · subst b
44     simp [selector_eval_self s hb]
45   · simp [h, selector_eval_other s hb h]
46 
47 variable [FiniteDimensional K V]
48 
49 /-- The actual finite eigenvalue set of T. -/
50 def eigenvalues (T : Module.End K V) : Finset K := T.finite_hasEigenvalue.toFinset
51 
52 theorem mem_eigenvalues (T : Module.End K V) (a : K) :
53     a ∈ eigenvalues T ↔ T.HasEigenvalue a := by
54   classical
55   simp [eigenvalues]
56 
57 /-- Evaluate the Lagrange selector on the actual operator. -/
58 def spectral (T : Module.End K V) (a : K) : Module.End K V :=
59   aeval T (selector (eigenvalues T) a)
60 
61 theorem spectral_absent (T : Module.End K V) (a : K) (ha : ¬ T.HasEigenvalue a) :
62     spectral T a = 0 := by
63   classical
64   simp [spectral, selector, mem_eigenvalues, ha]
65 
66 theorem spectral_on_eigenvector (T : Module.End K V) (a b : K) (x : V)
67     (hx : T x = b • x) : spectral T a x = if b = a then x else 0 := by
68   classical
69   by_cases hz : x = 0
70   · subst x; simp
71   have hb : b ∈ eigenvalues T := (mem_eigenvalues T b).2
72     (T.hasEigenvalue_of_hasEigenvector ⟨mem_eigenspace_iff.mpr hx, hz⟩)
73   rw [spectral, aeval_apply_of_mem_apply_eq_smul hx, selector_eval _ hb]
74   split_ifs <;> simp
75 
76 /-- Diagonalizability in the coefficient field: actual eigenspaces span V. -/
77 def Split (T : Module.End K V) : Prop := (⨆ a : K, T.eigenspace a) = ⊤
78 
79 theorem spectral_maps_into (T : Module.End K V) (hT : Split T) (a : K) (x : V) :
80     spectral T a x ∈ T.eigenspace a := by
81   have hle : (⨆ b : K, T.eigenspace b) ≤ (T.eigenspace a).comap (spectral T a) := by
82     refine iSup_le fun b => ?_
83     intro y hy
84     change spectral T a y ∈ T.eigenspace a
85     rw [spectral_on_eigenvector T a b y (mem_eigenspace_iff.mp hy)]
86     split_ifs with h
87     · simpa [h] using hy
88     · exact Submodule.zero_mem _
89   rw [hT] at hle
90   exact hle (Submodule.mem_top)
91 
92 theorem spectral_isProj (T : Module.End K V) (hT : Split T) (a : K) :
93     LinearMap.IsProj (T.eigenspace a) (spectral T a) := by
94   refine ⟨spectral_maps_into T hT a, ?_⟩
95   intro x hx
96   simpa using spectral_on_eigenvector T a a x (mem_eigenspace_iff.mp hx)
97 
98 theorem spectral_idempotent (T : Module.End K V) (hT : Split T) (a : K) :
99     IsIdempotentElem (spectral T a) := (spectral_isProj T hT a).isIdempotentElem
100 
101 theorem spectral_range (T : Module.End K V) (hT : Split T) (a : K) :
102     LinearMap.range (spectral T a) = T.eigenspace a := (spectral_isProj T hT a).range
103 
104 /-- The standard semisimple algebraically closed setting supplies Split. -/
105 theorem split_of_semisimple [IsAlgClosed K] (T : Module.End K V) (hT : T.IsSemisimple) :
106     Split T := hT.iSup_eigenspace_eq_top
107 
108 omit [FiniteDimensional K V] in
109 /-- Commutation survives evaluation of a polynomial in one operator. -/
110 theorem polynomial_commute_right (T U : Module.End K V) (h : Commute T U) (p : K[X]) :
111     Commute T (aeval U p) := by
112   induction p using Polynomial.induction_on' with
113   | add p q hp hq => simpa only [map_add] using hp.add_right hq
114   | monomial n c =>
115       rw [aeval_monomial]
116       exact (Algebra.commute_algebraMap_right c T).mul_right (h.pow_right n)
117 
118 theorem spectral_commute (T U : Module.End K V) (h : Commute T U) (a b : K) :
119     Commute (spectral T a) (spectral U b) := by
120   exact (polynomial_commute_right _ _
121     (polynomial_commute_right T U h (selector (eigenvalues U) b)).symm
122     (selector (eigenvalues T) a)).symm
123 
124 end PaperX.SpectralProjectors

Back to source controls