PacketIR.lean

1 module
2 
3 public import QuantumPacketCore
4 import all QuantumPacketCore
5 public import Mathlib.LinearAlgebra.Matrix.Kronecker
6 
7 /-!
8 Author: Komorebi P.
9 Paper VIII (strengthened edition), exact packet semantics, items 2.3, 2.5, 2.6.
10 The unchanged Paper VII module supplies the algebraic projector calculus.
11 Active addresses below mean exact nonzero blocks, not thresholded numerical tests.
12 -/
13 
14 public section
15 set_option autoImplicit false
16 set_option backward.isDefEq.respectTransparency false
17 set_option backward.isDefEq.respectTransparency.types false
18 namespace KomorebiPaperVIII
19 open scoped BigOperators
20 open KomorebiPaperVII
21 
22 section PacketSemantics
23 variable {R I : Type*} [Ring R] [Fintype I] [DecidableEq I]
24 variable (P : PacketFamily R I)
25 
26 /-- Target index precedes source index. The support is exact. -/
27 noncomputable def activeBlocks (A : R) : Finset (I × I) := by
28   classical
29   exact Finset.univ.filter (fun e => P.block A e.1 e.2 ≠ 0)
30 
31 /-- Evaluation of the stored nonzero packet blocks. -/
32 noncomputable def evalActive (A : R) : R :=
33   ∑ e ∈ activeBlocks P A, P.block A e.1 e.2
34 
35 theorem active_iff (A : R) (b a : I) :
36     (b, a) ∈ activeBlocks P A ↔ P.block A b a ≠ 0 := by
37   classical
38   simp [activeBlocks]
39 
40 /-- Theorem 2.3: removing exact zero blocks preserves the actual operator. -/
41 theorem exact_active_evaluation (A : R) : evalActive P A = A := by
42   classical
43   have term (e : I × I) :
44       (if P.block A e.1 e.2 ≠ 0 then P.block A e.1 e.2 else 0) =
45       P.block A e.1 e.2 := by
46     by_cases h : P.block A e.1 e.2 = 0 <;> simp [h]
47   simp only [evalActive, activeBlocks, Finset.sum_filter]
48   simp_rw [term]
49   simpa only [Fintype.sum_prod_type] using P.reconstruct A
50 
51 /-- The exact identity acts on arbitrary modules, including batches of columns. -/
52 theorem exact_active_action {M : Type*} [AddCommMonoid M] [Module R M]
53     (A : R) (x : M) : A • x = ∑ e ∈ activeBlocks P A, P.block A e.1 e.2 • x := by
54   rw [← Finset.sum_smul]
55   exact congrArg (fun a : R => a • x) (exact_active_evaluation P A).symm
56 
57 /-- Theorem 2.5: the actual product block, without assuming a sparsity pattern. -/
58 theorem exact_block_composition (A B : R) (b a : I) :
59     P.block (A * B) b a = ∑ c, P.block A b c * P.block B c a :=
60   P.compose_blocks A B b a
61 
62 /-- Support composition is an inclusion. Cancellation can make it strict. -/
63 theorem product_support_inclusion (A B : R) (b a : I)
64     (h : P.block (A * B) b a ≠ 0) :
65     ∃ c, P.block A b c ≠ 0 ∧ P.block B c a ≠ 0 := by
66   classical
67   by_contra no
68   apply h
69   rw [P.compose_blocks]
70   apply Finset.sum_eq_zero
71   intro c _
72   by_cases hc : P.block A b c = 0
73   · simp [hc]
74   · have hd : P.block B c a = 0 := by
75       by_contra hd
76       exact no ⟨c, hc, hd⟩
77     simp [hd]
78 
79 theorem block_sum {J : Type*} (s : Finset J) (A : J → R) (b a : I) :
80     P.block (∑ j ∈ s, A j) b a = ∑ j ∈ s, P.block (A j) b a := by
81   simp [PacketFamily.block, Finset.mul_sum, Finset.sum_mul]
82 
83 theorem all_blocks_zero (A : R) (h : ∀ b a, P.block A b a = 0) : A = 0 := by
84   rw [← P.reconstruct A]
85   simp [h]
86 
87 end PacketSemantics
88 
89 section Adjoint
90 variable {R I : Type*} [Ring R] [StarRing R] [Fintype I] [DecidableEq I]
91 variable (P : PacketFamily R I) (hstar : ∀ a, star (P.proj a) = P.proj a)
92 include hstar
93 
94 /-- Corollary 2.6, adjoint half. Self-adjointness of the packet projectors is explicit. -/
95 theorem exact_adjoint_block (A : R) (b a : I) :
96     star (P.block A b a) = P.block (star A) a b :=
97   P.adjoint_block hstar A b a
98 end Adjoint
99 
100 section Matrices
101 variable {K X Y I J : Type*} [CommRing K]
102 variable [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y]
103 variable [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J]
104 
105 /-- Actual coordinate projectors for any finite partition, with unequal or empty packets allowed. -/
106 def coordinatePackets (tag : X → I) : PacketFamily (Matrix X X K) I where
107   proj i := Matrix.diagonal (fun x => if tag x = i then 1 else 0)
108   mul_proj i j := by
109     rw [Matrix.diagonal_mul_diagonal]
110     by_cases h : i = j
111     · subst j
112       simp only [ite_true]
113       congr 1
114       funext x
115       by_cases hx : tag x = i <;> simp [hx]
116     · simp only [h, ite_false]
117       ext x y
118       by_cases hx : tag x = i
119       · simp [Matrix.diagonal_apply, hx, h]
120       · simp [Matrix.diagonal_apply, hx]
121   sum_proj := by
122     ext x y
123     by_cases h : x = y
124     · subst y
125       simp [Matrix.sum_apply]
126     · simp [Matrix.sum_apply, h]
127 
128 /-- Coordinate projectors act by retaining precisely one packet's entries. -/
129 theorem coordinate_projector_apply (tag : X → I) (i : I) (x : X → K) (u : X) :
130     ((coordinatePackets (K := K) tag).proj i).mulVec x u =
131       if tag u = i then x u else 0 := by
132   simp [coordinatePackets, Matrix.mulVec_diagonal]
133 
134 /-- Corollary 2.6, actual Kronecker-product block identity. -/
135 theorem exact_tensor_block (P : PacketFamily (Matrix X X K) I)
136     (Q : PacketFamily (Matrix Y Y K) J) (A : Matrix X X K) (B : Matrix Y Y K)
137     (b a : I) (d c : J) :
138     (Matrix.kroneckerMap (fun x y : K => x * y) (P.proj b) (Q.proj d)) * (Matrix.kroneckerMap (fun x y : K => x * y) A B) *
139       (Matrix.kroneckerMap (fun x y : K => x * y) (P.proj a) (Q.proj c)) =
140       Matrix.kroneckerMap (fun x y : K => x * y) (P.block A b a) (Q.block B d c) := by
141   rw [← Matrix.mul_kronecker_mul, ← Matrix.mul_kronecker_mul]
142   rfl
143 
144 /-- Explicit rectangular right-hand-side version of Theorem 2.3. -/
145 theorem exact_matrix_batch {C : Type*} (P : PacketFamily (Matrix X X K) I)
146     (A : Matrix X X K) (Z : Matrix X C K) :
147     A * Z = ∑ e ∈ activeBlocks P A, (P.block A e.1 e.2) * Z := by
148   rw [← Matrix.sum_mul]
149   exact congrArg (fun a : Matrix X X K => a * Z) (exact_active_evaluation P A).symm
150 end Matrices
151 
152 end KomorebiPaperVIII
153 
154 #print axioms KomorebiPaperVIII.active_iff
155 #print axioms KomorebiPaperVIII.exact_active_evaluation
156 #print axioms KomorebiPaperVIII.exact_active_action
157 #print axioms KomorebiPaperVIII.exact_block_composition
158 #print axioms KomorebiPaperVIII.product_support_inclusion
159 #print axioms KomorebiPaperVIII.block_sum
160 #print axioms KomorebiPaperVIII.all_blocks_zero
161 #print axioms KomorebiPaperVIII.exact_adjoint_block
162 #print axioms KomorebiPaperVIII.coordinate_projector_apply
163 #print axioms KomorebiPaperVIII.exact_tensor_block
164 #print axioms KomorebiPaperVIII.exact_matrix_batch
165 #print axioms KomorebiPaperVIII.coordinatePackets

Back to source controls