RequiredPacketOccupancy.lean

1 import PaperX.JointOccupancy
2 
3 /-! The positive trace of a spectral packet means its natural-number rank.
4 The field-valued trace is its cast, so this interpretation requires no order
5 on the coefficient field. Every required packet has its own witness. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperX.RequiredPacketOccupancy
9 
10 open PaperX.JointOccupancy PaperX.SpectralProjectors
11 
12 universe u v w x
13 
14 section OnePacket
15 
16 variable {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V]
17   [FiniteDimensional K V] {J : Type w}
18 
19 /-- The nonnegative integer measured by the actual spectral projector trace. -/
20 def naturalTrace (T : J → Module.End K V) (a : J → K) (indices : List J) : ℕ :=
21   Module.finrank K (jointSpace T a indices)
22 
23 /-- Positivity is the existence of a positive natural-number preimage of the
24 field trace. It is meaningful over characteristic-zero fields without an order. -/
25 def PositiveTrace (T : J → Module.End K V) (a : J → K) (indices : List J) : Prop :=
26   ∃ n : ℕ, 0 < n ∧ LinearMap.trace K V (joint T a indices) = (n : K)
27 
28 theorem naturalTrace_cast (T : J → Module.End K V) (a : J → K)
29     (hs : ∀ j, Split (T j)) (hc : ∀ i j, Commute (T i) (T j)) (indices : List J) :
30     (naturalTrace T a indices : K) = LinearMap.trace K V (joint T a indices) :=
31   (trace_eq_dimension T a hs hc indices).symm
32 
33 theorem naturalTrace_eq_of_cast [CharZero K] (T : J → Module.End K V) (a : J → K)
34     (hs : ∀ j, Split (T j)) (hc : ∀ i j, Commute (T i) (T j)) (indices : List J)
35     (n : ℕ) (hn : (n : K) = LinearMap.trace K V (joint T a indices)) :
36     n = naturalTrace T a indices :=
37   Nat.cast_injective (hn.trans (naturalTrace_cast T a hs hc indices).symm)
38 
39 theorem exists_unique_trace_integer [CharZero K] (T : J → Module.End K V)
40     (a : J → K) (hs : ∀ j, Split (T j)) (hc : ∀ i j, Commute (T i) (T j))
41     (indices : List J) :
42     ∃! n : ℕ, (n : K) = LinearMap.trace K V (joint T a indices) := by
43   exact ⟨naturalTrace T a indices, naturalTrace_cast T a hs hc indices,
44     fun n hn => naturalTrace_eq_of_cast T a hs hc indices n hn⟩
45 
46 theorem naturalTrace_pos_iff_occupied (T : J → Module.End K V) (a : J → K)
47     (indices : List J) :
48     0 < naturalTrace T a indices ↔ Occupied T a indices :=
49   (occupied_iff_dimension_pos T a indices).symm
50 
51 theorem naturalTrace_eq_zero_iff_not_occupied (T : J → Module.End K V) (a : J → K)
52     (indices : List J) :
53     naturalTrace T a indices = 0 ↔ ¬ Occupied T a indices := by
54   rw [← naturalTrace_pos_iff_occupied, Nat.not_lt, Nat.le_zero]
55 
56 theorem naturalTrace_pos_iff_fieldTrace_ne_zero [CharZero K]
57     (T : J → Module.End K V) (a : J → K) (hs : ∀ j, Split (T j))
58     (hc : ∀ i j, Commute (T i) (T j)) (indices : List J) :
59     0 < naturalTrace T a indices ↔ LinearMap.trace K V (joint T a indices) ≠ 0 :=
60   (naturalTrace_pos_iff_occupied T a indices).trans
61     (occupied_iff_trace_ne_zero T a hs hc indices)
62 
63 theorem naturalTrace_eq_zero_iff_fieldTrace_eq_zero [CharZero K]
64     (T : J → Module.End K V) (a : J → K) (hs : ∀ j, Split (T j))
65     (hc : ∀ i j, Commute (T i) (T j)) (indices : List J) :
66     naturalTrace T a indices = 0 ↔ LinearMap.trace K V (joint T a indices) = 0 := by
67   rw [← naturalTrace_cast T a hs hc indices, Nat.cast_eq_zero]
68 
69 theorem positiveTrace_iff_rank_pos [CharZero K]
70     (T : J → Module.End K V) (a : J → K) (hs : ∀ j, Split (T j))
71     (hc : ∀ i j, Commute (T i) (T j)) (indices : List J) :
72     PositiveTrace T a indices ↔ 0 < Module.finrank K (jointSpace T a indices) := by
73   constructor
74   · rintro ⟨n, hn, ht⟩
75     have heq := naturalTrace_eq_of_cast T a hs hc indices n ht.symm
76     change 0 < naturalTrace T a indices
77     rw [← heq]
78     exact hn
79   · intro h
80     exact ⟨naturalTrace T a indices, h, (naturalTrace_cast T a hs hc indices).symm⟩
81 
82 theorem occupied_iff_positiveTrace [CharZero K]
83     (T : J → Module.End K V) (a : J → K) (hs : ∀ j, Split (T j))
84     (hc : ∀ i j, Commute (T i) (T j)) (indices : List J) :
85     Occupied T a indices ↔ PositiveTrace T a indices :=
86   (occupied_iff_dimension_pos T a indices).trans
87     (positiveTrace_iff_rank_pos T a hs hc indices).symm
88 
89 theorem positiveTrace_iff_fieldTrace_ne_zero [CharZero K]
90     (T : J → Module.End K V) (a : J → K) (hs : ∀ j, Split (T j))
91     (hc : ∀ i j, Commute (T i) (T j)) (indices : List J) :
92     PositiveTrace T a indices ↔ LinearMap.trace K V (joint T a indices) ≠ 0 :=
93   (occupied_iff_positiveTrace T a hs hc indices).symm.trans
94     (occupied_iff_trace_ne_zero T a hs hc indices)
95 
96 end OnePacket
97 
98 section RequiredPackets
99 
100 variable {P : Type x} (K : P → Type u) (V : P → Type v) (J : P → Type w)
101   [∀ p, Field (K p)] [∀ p, AddCommGroup (V p)] [∀ p, Module (K p) (V p)]
102   [∀ p, FiniteDimensional (K p) (V p)]
103   (T : (p : P) → J p → Module.End (K p) (V p))
104   (a : (p : P) → J p → K p) (indices : (p : P) → List (J p))
105 
106 omit [∀ p, FiniteDimensional (K p) (V p)] in
107 /-- The index type need not be finite. Choice selects one witness in each of
108 the supplied carriers, without asserting that any two witnesses coincide. -/
109 theorem all_packets_iff_witnesses :
110     (∀ p, Occupied (T p) (a p) (indices p)) ↔
111     ∃ x : (p : P) → V p, ∀ p,
112       x p ≠ 0 ∧ ∀ i ∈ indices p, T p i (x p) = a p i • x p := by
113   constructor
114   · intro h
115     exact ⟨fun p => (h p).choose, fun p => (h p).choose_spec⟩
116   · rintro ⟨x, hx⟩ p
117     exact ⟨x p, hx p⟩
118 
119 theorem all_positive_iff_occupied :
120     (∀ p, 0 < naturalTrace (T p) (a p) (indices p)) ↔
121     ∀ p, Occupied (T p) (a p) (indices p) := by
122   exact forall_congr' fun p => naturalTrace_pos_iff_occupied (T p) (a p) (indices p)
123 
124 theorem all_positive_iff_witnesses :
125     (∀ p, 0 < naturalTrace (T p) (a p) (indices p)) ↔
126     ∃ x : (p : P) → V p, ∀ p,
127       x p ≠ 0 ∧ ∀ i ∈ indices p, T p i (x p) = a p i • x p :=
128   (all_positive_iff_occupied K V J T a indices).trans
129     (all_packets_iff_witnesses K V J T a indices)
130 
131 variable [∀ p, CharZero (K p)]
132   (hs : ∀ p j, Split (T p j)) (hc : ∀ p i j, Commute (T p i) (T p j))
133 
134 include hs hc
135 
136 theorem all_positive_iff_fieldTrace_ne_zero :
137     (∀ p, 0 < naturalTrace (T p) (a p) (indices p)) ↔
138     ∀ p, LinearMap.trace (K p) (V p) (joint (T p) (a p) (indices p)) ≠ 0 := by
139   exact forall_congr' fun p =>
140     naturalTrace_pos_iff_fieldTrace_ne_zero (T p) (a p) (hs p) (hc p) (indices p)
141 
142 theorem all_fieldTrace_ne_zero_iff_witnesses :
143     (∀ p, LinearMap.trace (K p) (V p) (joint (T p) (a p) (indices p)) ≠ 0) ↔
144     ∃ x : (p : P) → V p, ∀ p,
145       x p ≠ 0 ∧ ∀ i ∈ indices p, T p i (x p) = a p i • x p :=
146   (all_positive_iff_fieldTrace_ne_zero K V J T a indices hs hc).symm.trans
147     (all_positive_iff_witnesses K V J T a indices)
148 
149 theorem all_positiveTrace_iff_occupied :
150     (∀ p, PositiveTrace (T p) (a p) (indices p)) ↔
151     ∀ p, Occupied (T p) (a p) (indices p) := by
152   exact forall_congr' fun p => (occupied_iff_positiveTrace
153     (T p) (a p) (hs p) (hc p) (indices p)).symm
154 
155 theorem all_positiveTrace_iff_witnesses :
156     (∀ p, PositiveTrace (T p) (a p) (indices p)) ↔
157     ∃ x : (p : P) → V p, ∀ p,
158       x p ≠ 0 ∧ ∀ i ∈ indices p, T p i (x p) = a p i • x p :=
159   (all_positiveTrace_iff_occupied K V J T a indices hs hc).trans
160     (all_packets_iff_witnesses K V J T a indices)
161 
162 end RequiredPackets
163 
164 end PaperX.RequiredPacketOccupancy

Back to source controls