GraphSourceProjection.lean

1 import PaperIRelease.GraphPropagation
2 import PaperIRelease.PacketAggregation
3 
4 /-! Actual grouped source projections eliminate all incoming contributions
5 from outside the source SCC. This supplies the source-corner lower bound. -/
6 
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PaperIRelease
11 open Komorebi.Foundation
12 open Komorebi.PacketNaturalityCompletion.Reachability
13 open FiniteDigraph PacketAggregation
14 
15 universe u v w
16 variable {K : Type u} [Field K]
17 variable {X : Type v} [AddCommGroup X] [Module K X]
18 variable {I : Type w} [Fintype I] [DecidableEq I]
19 
20 /-- The actual grouped projector onto a strongly connected component. -/
21 abbrev componentProjection (P : LinearProjectorFamily K X I)
22     (ops : Set (Module.End K X)) (C : SCC (TransferEdge P ops)) : Module.End K X :=
23   (groupedFamily P (component (TransferEdge P ops))).proj C
24 
25 omit [DecidableEq I] in
26 theorem componentProjection_mem (P : LinearProjectorFamily K X I)
27     (ops : Set (Module.End K X)) (C : SCC (TransferEdge P ops)) :
28     componentProjection P ops C ∈ packetGeneratedAlgebra P ops := by
29   apply (packetGeneratedAlgebra P ops).sum_mem
30   intro a _
31   exact projector_mem_generatedAlgebra P ops a
32 
33 /-- The source projection of an operator depends only on the source projection
34 of its input. The operator is an element of the actual generated algebra. -/
35 theorem sourceProjection_compression (P : LinearProjectorFamily K X I)
36     (ops : Set (Module.End K X)) (C : Sources (TransferEdge P ops))
37     {T : Module.End K X} (hT : T ∈ packetGeneratedAlgebra P ops) (x : X) :
38     componentProjection P ops C.val (T x) =
39       componentProjection P ops C.val (T (componentProjection P ops C.val x)) := by
40   change groupedProjection P (component (TransferEdge P ops)) C.val (T x) =
41     groupedProjection P (component (TransferEdge P ops)) C.val
42       (T (groupedProjection P (component (TransferEdge P ops)) C.val x))
43   simp only [groupedProjection, LinearMap.sum_apply]
44   apply Finset.sum_congr rfl
45   intro b hb
46   have hbC := (Finset.mem_filter.mp hb).2
47   conv_lhs => rw [← P.complete x]
48   simp only [map_sum]
49   symm
50   apply Finset.sum_subset (Finset.filter_subset _ _)
51   intro a _ ha
52   have haC : component (TransferEdge P ops) a ≠ C.val := by
53     intro haC
54     exact ha (Finset.mem_filter.mpr ⟨Finset.mem_univ _, haC⟩)
55   exact LinearMap.congr_fun (source_block_zero P ops C haC hbC hT) x
56 
57 /-- Operator form of the same source-corner identity. -/
58 theorem sourceProjection_comp_eq (P : LinearProjectorFamily K X I)
59     (ops : Set (Module.End K X)) (C : Sources (TransferEdge P ops))
60     {T : Module.End K X} (hT : T ∈ packetGeneratedAlgebra P ops) :
61     (componentProjection P ops C.val).comp T =
62       ((componentProjection P ops C.val).comp T).comp (componentProjection P ops C.val) := by
63   ext x
64   exact sourceProjection_compression P ops C hT x
65 
66 omit [DecidableEq I] in
67 /-- A vector in a packet outside a component has zero component projection. -/
68 theorem componentProjection_other_packet (P : LinearProjectorFamily K X I)
69     (ops : Set (Module.End K X)) (C : SCC (TransferEdge P ops))
70     {a : I} (ha : component (TransferEdge P ops) a ≠ C) {x : X}
71     (hx : x ∈ LinearMap.range (P.proj a)) : componentProjection P ops C x = 0 := by
72   obtain ⟨y, rfl⟩ := hx
73   change (∑ i with component (TransferEdge P ops) i = C, P.proj i) (P.proj a y) = 0
74   rw [LinearMap.sum_apply]
75   apply Finset.sum_eq_zero
76   intro b hb
77   apply P.orthogonal
78   intro hba
79   exact ha (hba ▸ (Finset.mem_filter.mp hb).2)
80 
81 omit [DecidableEq I] in
82 /-- A vector in a packet of the component is fixed by its grouped projection. -/
83 theorem componentProjection_packet (P : LinearProjectorFamily K X I)
84     (ops : Set (Module.End K X)) (C : SCC (TransferEdge P ops))
85     {a : I} (ha : component (TransferEdge P ops) a = C) {x : X}
86     (hx : x ∈ LinearMap.range (P.proj a)) : componentProjection P ops C x = x := by
87   have hxC := original_mem_grouped P (component (TransferEdge P ops)) a ⟨x, hx⟩
88   rw [ha] at hxC
89   obtain ⟨y, hy⟩ := hxC
90   change componentProjection P ops C y = x at hy
91   rw [← hy]
92   exact (groupedFamily P (component (TransferEdge P ops))).idempotent C y
93 
94 end Komorebi.PaperIRelease

Back to source controls