AlgebraTransfer.lean

1 import KomorebiVerification.PacketNaturalityCompletion
2 
3 set_option autoImplicit false
4 set_option maxHeartbeats 2000000
5 
6 namespace Komorebi.PaperIRelease
7 open Komorebi.Foundation
8 
9 universe u v w
10 variable {K : Type u} [Field K]
11 variable {X : Type v} [AddCommGroup X] [Module K X]
12 variable {I : Type w} [Fintype I]
13 
14 /-- Lists are written in composition order: the rightmost operator acts first. -/
15 def operatorWord : List (Module.End K X) → Module.End K X
16   | [] => 1
17   | T :: ts => T.comp (operatorWord ts)
18 
19 /-- Recursive expansion over all intermediate packet indices for a nonidentical word. -/
20 noncomputable def packetWordSum (P : LinearProjectorFamily K X I) :
21     List (Module.End K X) → I → I → Module.End K X
22   | [], b, a => transferBlock P P 1 b a
23   | T :: ts, b, a => ∑ c, (transferBlock P P T b c).comp (packetWordSum P ts c a)
24 
25 theorem transferBlock_word (P : LinearProjectorFamily K X I)
26     (ts : List (Module.End K X)) (b a : I) :
27     transferBlock P P (operatorWord ts) b a = packetWordSum P ts b a := by
28   induction ts generalizing b a with
29   | nil => rfl
30   | cons T ts ih =>
31     simp only [operatorWord, packetWordSum, transferBlock_comp_end, ih]
32 
33 def packetSupport (P : LinearProjectorFamily K X I) (x : X) : Set I :=
34   {i | P.proj i x ≠ 0}
35 
36 def PacketPure (P : LinearProjectorFamily K X I) (x : X) : Prop :=
37   (packetSupport P x).Subsingleton
38 
39 /-- Zero vectors have empty support and are packet pure. -/
40 theorem packetPure_zero (P : LinearProjectorFamily K X I) : PacketPure P (0 : X) := by
41   intro a ha
42   exact (ha (map_zero _)).elim
43 
44 /-- A vector in one projector range has no other packet component. -/
45 theorem packetPure_of_mem_range (P : LinearProjectorFamily K X I) {i : I} {x : X}
46     (hx : x ∈ LinearMap.range (P.proj i)) : PacketPure P x := by
47   rintro a ha b hb
48   obtain ⟨y, rfl⟩ := hx
49   have hai : a = i := by
50     by_contra h
51     exact ha (P.orthogonal h y)
52   have hbi : b = i := by
53     by_contra h
54     exact hb (P.orthogonal h y)
55   exact hai.trans hbi.symm
56 
57 /-- Nonzero packet-pure vectors belong to their unique active packet. -/
58 theorem packetPure_mem_range (P : LinearProjectorFamily K X I) {x : X}
59     (hx : PacketPure P x) {i : I} (hi : i ∈ packetSupport P x) :
60     x ∈ LinearMap.range (P.proj i) := by
61   classical
62   have heq : x = P.proj i x := by
63     calc
64       x = ∑ j, P.proj j x := (P.complete x).symm
65       _ = P.proj i x := by
66         apply Finset.sum_eq_single i
67         · intro j _ hji
68           by_contra hj
69           exact hji (hx hj hi)
70         · simp
71   exact ⟨x, heq.symm⟩
72 
73 /-- Packet purity is exactly zero or membership in one actual packet range. -/
74 theorem packetPure_iff_zero_or_range (P : LinearProjectorFamily K X I) (x : X) :
75     PacketPure P x ↔ x = 0 ∨ ∃ i, x ∈ LinearMap.range (P.proj i) := by
76   classical
77   constructor
78   · intro hx
79     by_cases h : ∃ i, P.proj i x ≠ 0
80     · obtain ⟨i, hi⟩ := h
81       exact Or.inr ⟨i, packetPure_mem_range P hx hi⟩
82     · left
83       apply P.eq_of_projectors_eq
84       intro i
85       have hi : P.proj i x = 0 := by by_contra hi; exact h ⟨i, hi⟩
86       simpa only [map_zero] using hi
87   · rintro (rfl | ⟨i, hi⟩)
88     · exact packetPure_zero P
89     · exact packetPure_of_mem_range P hi
90 
91 def activeTargets (P : LinearProjectorFamily K X I) (T : Module.End K X) (x : X) : Set I :=
92   {b | ∃ a, a ∈ packetSupport P x ∧ transferBlock P P T b a ≠ 0}
93 
94 /-- Each target coordinate is the exact sum of source-coordinate contributions. -/
95 theorem target_coordinate_sum (P : LinearProjectorFamily K X I)
96     (T : Module.End K X) (x : X) (b : I) :
97     P.proj b (T x) = ∑ a, transferBlock P P T b a (P.proj a x) := by
98   simp only [transferBlock, LinearMap.comp_apply, P.idempotent]
99   rw [← map_sum, ← map_sum, P.complete]
100 
101 theorem packetSupport_image_subset (P : LinearProjectorFamily K X I)
102     (T : Module.End K X) (x : X) :
103     packetSupport P (T x) ⊆ activeTargets P T x := by
104   intro b hb
105   by_contra h
106   apply hb
107   rw [target_coordinate_sum]
108   apply Finset.sum_eq_zero
109   intro a _
110   by_cases ha : a ∈ packetSupport P x
111   · have hzero : transferBlock P P T b a = 0 := by
112       by_contra hne
113       exact h ⟨a, ha, hne⟩
114     rw [hzero, LinearMap.zero_apply]
115   · have hzero : P.proj a x = 0 := not_not.mp ha
116     rw [hzero, map_zero]
117 
118 noncomputable def activeSources (P : LinearProjectorFamily K X I)
119     (T : Module.End K X) (x : X) (b : I) : Finset I := by
120   classical
121   exact Finset.univ.filter (fun a => P.proj a x ≠ 0 ∧ transferBlock P P T b a ≠ 0)
122 
123 theorem target_coordinate_active_sum (P : LinearProjectorFamily K X I)
124     (T : Module.End K X) (x : X) (b : I) :
125     P.proj b (T x) =
126       ∑ a ∈ activeSources P T x b, transferBlock P P T b a (P.proj a x) := by
127   classical
128   rw [target_coordinate_sum]
129   symm
130   apply Finset.sum_subset (Finset.subset_univ _)
131   intro a _ ha
132   have hn : ¬ (P.proj a x ≠ 0 ∧ transferBlock P P T b a ≠ 0) := by
133     simpa only [activeSources, Finset.mem_filter, Finset.mem_univ, true_and] using ha
134   by_cases hx : P.proj a x = 0
135   · rw [hx, map_zero]
136   · have hzero : transferBlock P P T b a = 0 := by tauto
137     rw [hzero, LinearMap.zero_apply]
138 
139 /-- Equality holds precisely under the stated no-cancellation condition at each active target. -/
140 theorem packetSupport_image_eq_of_noncancellation (P : LinearProjectorFamily K X I)
141     (T : Module.End K X) (x : X)
142     (h : ∀ b ∈ activeTargets P T x,
143       (∑ a ∈ activeSources P T x b, transferBlock P P T b a (P.proj a x)) ≠ 0) :
144     packetSupport P (T x) = activeTargets P T x := by
145   apply Set.Subset.antisymm (packetSupport_image_subset P T x)
146   intro b hb
147   change P.proj b (T x) ≠ 0
148   rw [target_coordinate_active_sum]
149   exact h b hb
150 
151 /-- At most one active source with nonzero contribution is sufficient. -/
152 theorem packetSupport_image_eq_of_single_active (P : LinearProjectorFamily K X I)
153     (T : Module.End K X) (x : X)
154     (h : ∀ b ∈ activeTargets P T x, ∃ a,
155       activeSources P T x b = {a} ∧ transferBlock P P T b a (P.proj a x) ≠ 0) :
156     packetSupport P (T x) = activeTargets P T x := by
157   classical
158   apply packetSupport_image_eq_of_noncancellation
159   intro b hb
160   obtain ⟨a, ha, hne⟩ := h b hb
161   simpa [ha] using hne
162 
163 end Komorebi.PaperIRelease

Back to source controls