OccupancyExamples.lean

1 import PaperX.JointOccupancy
2 
3 /-! Actual split operators and the rank sequence 3,2,1,0. Every individual
4 selected eigenvalue is present, but their joint packet can be empty. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.OccupancyExamples
8 
9 open scoped BigOperators Matrix
10 open LinearMap Module.End PaperX.SpectralProjectors PaperX.JointOccupancy
11 attribute [local instance] Classical.propDecidable
12 universe u v
13 variable {K : Type u} [Field K] {J : Type v} [Fintype J] [DecidableEq J]
14 
15 /-- Diagonal coordinate multiplication is an actual linear endomorphism. -/
16 def diagOp (c : J → K) : Module.End K (J → K) :=
17   LinearMap.pi fun j => c j • LinearMap.proj j
18 
19 omit [Fintype J] [DecidableEq J] in
20 theorem diag_apply (c x : J → K) (j : J) : diagOp c x j = c j * x j := rfl
21 
22 theorem diag_basis (c : J → K) (j : J) :
23     diagOp c (Pi.basisFun K J j) = c j • Pi.basisFun K J j := by
24   ext i
25   simp [diagOp, Pi.basisFun_apply, Pi.single_apply]
26   split_ifs with h
27   · subst i; rfl
28   · simp
29 
30 theorem diag_split (c : J → K) : Split (diagOp c) := by
31   apply top_unique
32   rw [← (Pi.basisFun K J).span_eq]
33   apply Submodule.span_le.mpr
34   rintro _ ⟨j,rfl⟩
35   exact (le_iSup (fun a : K => (diagOp c).eigenspace a) (c j))
36     (mem_eigenspace_iff.mpr (diag_basis c j))
37 
38 theorem diag_commute (c d : J → K) : Commute (diagOp c) (diagOp d) := by
39   ext x j
40   simp [Module.End.mul_apply, diag_apply, mul_left_comm]
41 
42 theorem diag_mul (c d : J → K) : diagOp c * diagOp d = diagOp (fun j => c j * d j) := by
43   ext x j
44   simp [Module.End.mul_apply, diag_apply, mul_assoc]
45 
46 theorem diag_one : diagOp (fun _ : J => (1 : K)) = 1 := by
47   ext x j
48   simp [diag_apply]
49 
50 theorem spectral_diag (c : J → K) (a : K) :
51     spectral (diagOp c) a = diagOp (fun j => if c j = a then 1 else 0) := by
52   apply (Pi.basisFun K J).ext
53   intro j
54   rw [spectral_on_eigenvector _ a (c j) _ (diag_basis c j), diag_basis]
55   split_ifs <;> simp
56 
57 /-- The full diagonal trace calculation, not a rank assigned by definition. -/
58 theorem trace_diag (c : J → K) : LinearMap.trace K (J → K) (diagOp c) = ∑ j, c j := by
59   rw [LinearMap.trace_eq_matrix_trace K (Pi.basisFun K J)]
60   simp [Matrix.trace, diag_apply]
61 
62 /-- Four conditions, all individually feasible. -/
63 def values : Fin 4 → Fin 4 → ℚ :=
64   ![![1,1,1,0], ![2,2,0,0], ![3,0,0,0], ![0,4,4,4]]
65 
66 def target : Fin 4 → ℚ := ![1,2,3,4]
67 
68 def operators (i : Fin 4) : Module.End ℚ (Fin 4 → ℚ) := diagOp (values i)
69 
70 def masks : Fin 4 → Fin 4 → ℚ :=
71   ![![1,1,1,0], ![1,1,0,0], ![1,0,0,0], ![0,1,1,1]]
72 
73 theorem actual_projectors (i : Fin 4) : spectral (operators i) (target i) = diagOp (masks i) := by
74   rw [operators, spectral_diag]
75   congr 1
76   fin_cases i <;> ext j <;> fin_cases j <;> norm_num [values,target,masks]
77 
78 theorem all_targets_present (i : Fin 4) : (operators i).HasEigenvalue (target i) := by
79   have h (j : Fin 4) (hc : values i j = target i) : (operators i).HasEigenvalue (target i) := by
80     exact (operators i).hasEigenvalue_of_hasEigenvector
81       ⟨mem_eigenspace_iff.mpr (hc ▸ diag_basis (values i) j), (Pi.basisFun ℚ (Fin 4)).ne_zero j⟩
82   fin_cases i
83   · exact h 0 (by norm_num [values,target])
84   · exact h 0 (by norm_num [values,target])
85   · exact h 0 (by norm_num [values,target])
86   · exact h 1 (by norm_num [values,target])
87 
88 theorem projector_prefixes :
89     joint operators target [0] = diagOp ![1,1,1,0] ∧
90     joint operators target [0,1] = diagOp ![1,1,0,0] ∧
91     joint operators target [0,1,2] = diagOp ![1,0,0,0] ∧
92     joint operators target [0,1,2,3] = 0 := by
93   simp only [joint_cons, joint_nil, mul_one, actual_projectors, diag_mul]
94   refine ⟨rfl, ?_, ?_, ?_⟩
95   · apply congrArg diagOp; decide +kernel
96   · apply congrArg diagOp; decide +kernel
97   · ext x j; fin_cases j <;> simp [diag_apply,masks]
98 
99 theorem occupancy_traces :
100     LinearMap.trace ℚ (Fin 4 → ℚ) (joint operators target [0]) = 3 ∧
101     LinearMap.trace ℚ (Fin 4 → ℚ) (joint operators target [0,1]) = 2 ∧
102     LinearMap.trace ℚ (Fin 4 → ℚ) (joint operators target [0,1,2]) = 1 ∧
103     LinearMap.trace ℚ (Fin 4 → ℚ) (joint operators target [0,1,2,3]) = 0 := by
104   rcases projector_prefixes with ⟨h1,h2,h3,h4⟩
105   rw [h1,h2,h3,h4]
106   norm_num [trace_diag, Fin.sum_univ_succ]
107 
108 theorem occupancy_dimensions :
109     Module.finrank ℚ (jointSpace operators target [0]) = 3 ∧
110     Module.finrank ℚ (jointSpace operators target [0,1]) = 2 ∧
111     Module.finrank ℚ (jointSpace operators target [0,1,2]) = 1 ∧
112     Module.finrank ℚ (jointSpace operators target [0,1,2,3]) = 0 := by
113   have htr := occupancy_traces
114   simp only [trace_eq_dimension operators target (fun i => diag_split (values i))
115     (fun i j => diag_commute (values i) (values j))] at htr
116   exact_mod_cast htr
117 
118 theorem joint_packet_empty : ¬ Occupied operators target [0,1,2,3] := by
119   rw [occupied_iff_trace_ne_zero operators target (fun i => diag_split (values i))
120     (fun i j => diag_commute (values i) (values j))]
121   simp [occupancy_traces.2.2.2]
122 
123 theorem smaller_packet_occupied : Occupied operators target [0,1,2] := by
124   rw [occupied_iff_trace_ne_zero operators target (fun i => diag_split (values i))
125     (fun i j => diag_commute (values i) (values j)), occupancy_traces.2.2.1]
126   norm_num
127 
128 end PaperX.OccupancyExamples

Back to source controls