PacketAggregation.lean

1 import KomorebiVerification.ExactCoordinates
2 
3 set_option autoImplicit false
4 set_option linter.unusedSectionVars false
5 noncomputable section
6 namespace Komorebi.PaperIRelease.PacketAggregation
7 open Komorebi.Foundation Komorebi.Foundation.LinearProjectorFamily
8 universe u v w x
9 variable {R : Type u} [CommSemiring R]
10 variable {M : Type v} [AddCommMonoid M] [Module R M]
11 variable {ι : Type w} [Fintype ι] {κ : Type x} [Fintype κ] [DecidableEq κ]
12 variable (P : LinearProjectorFamily R M ι) (σ : ι → κ)
13 
14 /-- Actual sum of the original projectors in a fibre. -/
15 def groupedProjection (j : κ) : Module.End R M := ∑ i with σ i = j, P.proj i
16 
17 theorem proj_groupedProjection (a : ι) (j : κ) (m : M) :
18     P.proj a (groupedProjection P σ j m) = if σ a = j then P.proj a m else 0 := by
19   classical
20   simp only [groupedProjection, LinearMap.sum_apply, map_sum]
21   by_cases ha : σ a = j
22   · rw [ite_eq_left ha, Finset.sum_eq_single a]
23     · exact P.idempotent a m
24     · intro b _ hba
25       exact P.orthogonal hba.symm m
26     · simp [ha]
27   · rw [ite_eq_right ha]
28     apply Finset.sum_eq_zero
29     intro b hb
30     have hba : a ≠ b := by
31       intro hab
32       exact ha (hab ▸ (Finset.mem_filter.mp hb).2)
33     exact P.orthogonal hba m
34 
35 /-- Finite fibre sums form a complete orthogonal projector family. -/
36 def groupedFamily : LinearProjectorFamily R M κ where
37   proj := groupedProjection P σ
38   idempotent j m := by
39     simp only [groupedProjection, LinearMap.sum_apply]
40     apply Finset.sum_congr rfl
41     intro a ha
42     have h := proj_groupedProjection P σ a j m
43     simpa only [groupedProjection, LinearMap.sum_apply, ite_eq_left (Finset.mem_filter.mp ha).2] using h
44   orthogonal {j k} hjk m := by
45     change (∑ a with σ a = j, P.proj a) (groupedProjection P σ k m) = 0
46     rw [LinearMap.sum_apply]
47     apply Finset.sum_eq_zero
48     intro a ha
49     rw [proj_groupedProjection, ite_eq_right]
50     exact fun hak => hjk ((Finset.mem_filter.mp ha).2.symm.trans hak)
51   complete m := by
52     simp only [groupedProjection, LinearMap.sum_apply]
53     have h := Finset.sum_fiberwise_eq_sum_filter Finset.univ Finset.univ σ (fun i => P.proj i m)
54     simpa only [Finset.mem_univ, Finset.filter_true_of_mem, Finset.sum_const_zero] using h.trans (by simpa using P.complete m)
55 
56 /-- An original packet lies in its grouped range. -/
57 theorem original_mem_grouped (a : ι) (m : (P.proj a).range) :
58     (m : M) ∈ ((groupedFamily P σ).proj (σ a)).range := by
59   classical
60   refine ⟨m, ?_⟩
61   change groupedProjection P σ (σ a) m = m
62   simp only [groupedProjection, LinearMap.sum_apply]
63   rw [Finset.sum_eq_single a]
64   · obtain ⟨x, hx⟩ := m.property
65     rw [← hx]
66     exact P.idempotent a x
67   · intro b _ hba
68     obtain ⟨x, hx⟩ := m.property
69     rw [← hx]
70     exact P.orthogonal hba x
71   · simp
72 
73 /-- Surjective grouping preserves nonzero packets. -/
74 theorem grouped_nonzero (hP : ∀ i, P.proj i ≠ 0) (hσ : Function.Surjective σ) :
75     ∀ j, (groupedFamily P σ).proj j ≠ 0 := by
76   intro j hj
77   obtain ⟨i, rfl⟩ := hσ j
78   apply hP i
79   ext m
80   have h := original_mem_grouped P σ i ⟨P.proj i m, ⟨m, rfl⟩⟩
81   rw [hj] at h
82   simpa using h
83 
84 
85 /-- Actual packet coordinates inside one grouped range. -/
86 def groupedAnalysis (j : κ) : ((groupedFamily P σ).proj j).range →ₗ[R]
87     ((i : {i : ι // σ i = j}) → (P.proj i.val).range) where
88   toFun m i := ⟨P.proj i.val m, ⟨m, rfl⟩⟩
89   map_add' _ _ := by ext i; simp
90   map_smul' _ _ := by ext i; simp
91 
92 /-- Synthesis of the original packets in a single fibre. -/
93 def groupedSynthesis (j : κ) :
94     ((i : {i : ι // σ i = j}) → (P.proj i.val).range) →ₗ[R]
95       ((groupedFamily P σ).proj j).range where
96   toFun m := ⟨∑ i, (m i : M), by
97     apply Submodule.sum_mem
98     intro i _
99     have h := original_mem_grouped P σ i.val (m i)
100     simpa only [i.property] using h⟩
101   map_add' _ _ := by apply Subtype.ext; simp [Finset.sum_add_distrib]
102   map_smul' _ _ := by apply Subtype.ext; simp [Finset.smul_sum]
103 
104 @[simp] theorem groupedSynthesis_analysis (j : κ)
105     (m : ((groupedFamily P σ).proj j).range) :
106     groupedSynthesis P σ j (groupedAnalysis P σ j m) = m := by
107   apply Subtype.ext
108   change (∑ i : {i : ι // σ i = j}, P.proj i.val m) = m
109   have hs := Finset.sum_subtype (p := fun i => σ i = j) (F := inferInstance) (Finset.univ.filter (fun i => σ i = j))
110     (by intro i; simp) (fun i => P.proj i m)
111   rw [← hs]
112   have hm : groupedProjection P σ j m = m := by
113     obtain ⟨x, hx⟩ := m.property
114     rw [← hx]
115     exact (groupedFamily P σ).idempotent j x
116   simpa only [groupedProjection, LinearMap.sum_apply] using hm
117 
118 @[simp] theorem groupedAnalysis_synthesis (j : κ)
119     (m : (i : {i : ι // σ i = j}) → (P.proj i.val).range) :
120     groupedAnalysis P σ j (groupedSynthesis P σ j m) = m := by
121   classical
122   funext a
123   apply Subtype.ext
124   change P.proj a.val (∑ i, (m i : M)) = m a
125   rw [map_sum, Finset.sum_eq_single a]
126   · obtain ⟨x, hx⟩ := (m a).property
127     rw [← hx]
128     exact P.idempotent a.val x
129   · intro b _ hba
130     obtain ⟨x, hx⟩ := (m b).property
131     rw [← hx]
132     exact P.orthogonal (fun hab => hba (Subtype.ext hab.symm)) x
133   · simp
134 
135 /-- The grouped range is canonically the product of the actual original packet ranges. -/
136 def groupedRangeEquiv (j : κ) : ((groupedFamily P σ).proj j).range ≃ₗ[R]
137     ((i : {i : ι // σ i = j}) → (P.proj i.val).range) where
138   toFun := groupedAnalysis P σ j
139   invFun := groupedSynthesis P σ j
140   left_inv := groupedSynthesis_analysis P σ j
141   right_inv := groupedAnalysis_synthesis P σ j
142   map_add' := (groupedAnalysis P σ j).map_add
143   map_smul' := (groupedAnalysis P σ j).map_smul
144 
145 /-- Literal finite direct-sum form of packet aggregation. -/
146 def groupedRangeDirectSumEquiv (j : κ) : ((groupedFamily P σ).proj j).range ≃ₗ[R]
147     DirectSum {i : ι // σ i = j} (fun i => (P.proj i.val).range) := by
148   classical
149   exact (groupedRangeEquiv P σ j).trans
150     (DirectSum.linearEquivFunOnFintype R _ _).symm
151 
152 end Komorebi.PaperIRelease.PacketAggregation

Back to source controls