OccupancyBoundary.lean

1 import PaperX.OccupancyExamples
2 
3 /-! Exact counterexamples to dropping diagonalizability or commutation.
4 These refute proposed stronger finite statements, not universal occupancy. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.OccupancyBoundary
8 
9 open scoped Matrix Polynomial
10 open Polynomial Module.End PaperX.SpectralProjectors
11 
12 def jordan : Matrix (Fin 2) (Fin 2) ℚ := !![1,1;0,1]
13 def jordanOp : Module.End ℚ (Fin 2 → ℚ) := jordan.toLin'
14 
15 def P : Matrix (Fin 2) (Fin 2) ℚ := !![1,0;0,0]
16 def Q : Matrix (Fin 2) (Fin 2) ℚ := !![1/2,1/2;1/2,1/2]
17 
18 theorem individual_idempotents : P*P = P ∧ Q*Q = Q := by decide +kernel
19 
20 theorem noncommuting : P*Q ≠ Q*P := by decide +kernel
21 
22 theorem product_not_idempotent : (P*Q)*(P*Q) ≠ P*Q := by decide +kernel
23 
24 theorem product_trace_half : (P*Q).trace = 1/2 := by decide +kernel
25 
26 theorem jordan_eigenvectors (a : ℚ) (x : Fin 2 → ℚ)
27     (hx : jordan *ᵥ x = a • x) : (a = 1 ∧ x 1 = 0) ∨ x = 0 := by
28   have h0 := congrFun hx 0
29   have h1 := congrFun hx 1
30   simp [jordan, Matrix.mulVec, dotProduct, Fin.sum_univ_succ] at h0 h1
31   by_cases h : a = 1
32   · left; constructor
33     · exact h
34     · subst a; linarith
35   · have hz1 : x 1 = 0 := by
36       have hm : (a-1)*x 1 = 0 := by linarith
37       exact (mul_eq_zero.mp hm).resolve_left (sub_ne_zero.mpr h)
38     have hz0 : x 0 = 0 := by
39       have hm : (a-1)*x 0 = 0 := by rw [hz1] at h0; linarith
40       exact (mul_eq_zero.mp hm).resolve_left (sub_ne_zero.mpr h)
41     right; ext i; fin_cases i <;> assumption
42 
43 theorem jordan_eigenvalue_iff (a : ℚ) : jordanOp.HasEigenvalue a ↔ a = 1 := by
44   constructor
45   · intro ha
46     obtain ⟨x,hx,hne⟩ := (Submodule.ne_bot_iff _).mp ha
47     exact (jordan_eigenvectors a x (mem_eigenspace_iff.mp hx)).resolve_right hne |>.1
48   · rintro rfl
49     exact jordanOp.hasEigenvalue_of_hasEigenvector
50       ⟨mem_eigenspace_iff.mpr (show jordan *ᵥ ![(1:ℚ),0] = 1 • ![1,0] by decide +kernel),
51        by decide +kernel⟩
52 
53 theorem jordan_spectrum : eigenvalues jordanOp = {1} := by
54   ext a
55   simp [mem_eigenvalues, jordan_eigenvalue_iff]
56 
57 /-- On the Jordan block, the literal singleton Lagrange formula is the identity,
58 not the projector onto the one-dimensional eigenspace. -/
59 theorem jordan_spectral_identity : spectral jordanOp 1 = 1 := by
60   simp [spectral, jordan_spectrum, selector]
61 
62 theorem jordan_formula_wrong_image :
63     ∃ x : Fin 2 → ℚ, spectral jordanOp 1 x ∉ jordanOp.eigenspace 1 := by
64   refine ⟨![0,1], ?_⟩
65   rw [jordan_spectral_identity]
66   rw [mem_eigenspace_iff]
67   change ¬ jordan *ᵥ ![(0:ℚ),1] = 1 • ![0,1]
68   decide +kernel
69 
70 theorem jordan_not_split : ¬ Split jordanOp := by
71   intro h
72   obtain ⟨x,hx⟩ := jordan_formula_wrong_image
73   exact hx (spectral_maps_into jordanOp h 1 x)
74 
75 end PaperX.OccupancyBoundary

Back to source controls