OccupancyTransport.lean

1 import PaperX.JointOccupancy
2 
3 /-! Naturality under actual intertwiners. This includes invariance under a
4 change of basis, without assuming that the operators are coordinate-diagonal. -/
5 set_option autoImplicit false
6 noncomputable section
7 namespace PaperX.OccupancyTransport
8 
9 open LinearMap Module.End PaperX.SpectralProjectors PaperX.JointOccupancy
10 attribute [local instance] Classical.propDecidable
11 universe u v w z
12 variable {K : Type u} [Field K]
13   {V : Type v} [AddCommGroup V] [Module K V] [FiniteDimensional K V]
14   {W : Type w} [AddCommGroup W] [Module K W] [FiniteDimensional K W]
15   {I : Type z}
16 
17 /-- Any intertwiner respects the actual Lagrange projectors when the source
18 operator is split. The target need not have the identical full spectrum. -/
19 theorem spectral_intertwines (T : Module.End K V) (U : Module.End K W)
20     (F : V →ₗ[K] W) (hT : Split T) (hF : U.comp F = F.comp T) (a : K) :
21     (spectral U a).comp F = F.comp (spectral T a) := by
22   have hle : (⨆ b : K, T.eigenspace b) ≤
23       LinearMap.ker ((spectral U a).comp F - F.comp (spectral T a)) := by
24     refine iSup_le fun b => ?_
25     intro x hx
26     have hx' : T x = b • x := mem_eigenspace_iff.mp hx
27     have hfx : U (F x) = b • F x := by
28       have he := LinearMap.congr_fun hF x
29       simpa only [LinearMap.comp_apply, hx', map_smul] using he
30     change spectral U a (F x) - F (spectral T a x) = 0
31     rw [spectral_on_eigenvector U a b (F x) hfx,
32       spectral_on_eigenvector T a b x hx']
33     split_ifs <;> simp
34   rw [hT] at hle
35   exact sub_eq_zero.mp (LinearMap.ker_eq_top.mp (top_unique hle))
36 
37 theorem joint_intertwines (T : I → Module.End K V) (U : I → Module.End K W)
38     (F : V →ₗ[K] W) (hs : ∀ i, Split (T i))
39     (hF : ∀ i, (U i).comp F = F.comp (T i)) (a : I → K) (l : List I) :
40     (joint U a l).comp F = F.comp (joint T a l) := by
41   induction l with
42   | nil => ext x; rfl
43   | cons i l ih =>
44     ext x
45     have he := LinearMap.congr_fun (spectral_intertwines (T i) (U i) F (hs i) (hF i) (a i))
46       (joint T a l x)
47     have hl := LinearMap.congr_fun ih x
48     change spectral (U i) (a i) (joint U a l (F x)) = F (spectral (T i) (a i) (joint T a l x))
49     change joint U a l (F x) = F (joint T a l x) at hl
50     rw [hl]
51     exact he
52 
53 theorem joint_conjugate (T : I → Module.End K V) (U : I → Module.End K W)
54     (e : V ≃ₗ[K] W) (hs : ∀ i, Split (T i))
55     (he : ∀ i, (U i).comp e.toLinearMap = e.toLinearMap.comp (T i))
56     (a : I → K) (l : List I) :
57     joint U a l = (e.toLinearMap.comp (joint T a l)).comp e.symm.toLinearMap := by
58   ext x
59   have h := LinearMap.congr_fun (joint_intertwines T U e.toLinearMap hs he a l) (e.symm x)
60   simpa using h
61 
62 /-- A basis change preserves the actual field-valued trace. -/
63 theorem trace_conjugate (T : I → Module.End K V) (U : I → Module.End K W)
64     (e : V ≃ₗ[K] W) (hs : ∀ i, Split (T i))
65     (he : ∀ i, (U i).comp e.toLinearMap = e.toLinearMap.comp (T i))
66     (a : I → K) (l : List I) :
67     LinearMap.trace K W (joint U a l) = LinearMap.trace K V (joint T a l) := by
68   rw [joint_conjugate T U e hs he a l, LinearMap.trace_comp_comm']
69   simp
70 
71 end PaperX.OccupancyTransport

Back to source controls