TensorRefinement.lean

1 module
2 public import Mathlib.LinearAlgebra.Matrix.ConjTranspose
3 public import Mathlib.Algebra.BigOperators.Ring.Finset
4 public import Mathlib.Data.Fintype.Pi
5 public import Mathlib.Data.ZMod.Basic
6 public import Mathlib.Analysis.Complex.Basic
7 /-! Author: Komorebi P. Paper VII second block, Theorem 3.2.
8 Arbitrary finite tensor products and regrouping by total residue. -/
9 public section
10 set_option autoImplicit false
11 namespace KomorebiPaperVII.TensorRefinement
12 open scoped BigOperators
13 section Tensor
14 variable {F : Type*} [Fintype F] [DecidableEq F]
15   {D : F → Type*} [∀ i, Fintype (D i)]
16 def tensor (A : (i : F) → Matrix (D i) (D i) ℂ) :
17     Matrix ((i : F) → D i) ((i : F) → D i) ℂ :=
18   fun x y => ∏ i, A i (x i) (y i)
19 
20 theorem tensor_mul (A B : (i : F) → Matrix (D i) (D i) ℂ) :
21     tensor (fun i => A i * B i) = tensor A * tensor B := by
22   ext x y
23   simp only [tensor, Matrix.mul_apply]
24   rw [Fintype.prod_sum]
25   apply Finset.sum_congr rfl
26   intro z _
27   exact Finset.prod_mul_distrib
28 
29 omit [∀ i, Fintype (D i)] [DecidableEq F] in
30 theorem tensor_one [∀ i, DecidableEq (D i)] :
31     tensor (fun i => (1 : Matrix (D i) (D i) ℂ)) = 1 := by
32   classical
33   ext x y
34   by_cases h : x = y
35   · subst y
36     simp [tensor]
37   · simp only [tensor, Matrix.one_apply, h, ite_false]
38     obtain ⟨i, hi⟩ := Function.ne_iff.mp h
39     exact Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi])
40 
41 omit [∀ i, Fintype (D i)] in
42 theorem tensor_sum {J : F → Type*} [∀ i, Fintype (J i)]
43     (P : (i : F) → J i → Matrix (D i) (D i) ℂ) :
44     (∑ a : (i : F) → J i, tensor (fun i => P i (a i))) =
45       tensor (fun i => ∑ j, P i j) := by
46   ext x y
47   simp only [Matrix.sum_apply]
48   change (∑ a : (i : F) → J i, ∏ i, P i (a i) (x i) (y i)) =
49     ∏ i, (∑ j, P i j) (x i) (y i)
50   simp only [Matrix.sum_apply]
51   exact (Fintype.prod_sum (fun i j => P i j (x i) (y i))).symm
52 
53 omit [∀ i, Fintype (D i)] [DecidableEq F] in
54 theorem tensor_adjoint (A : (i : F) → Matrix (D i) (D i) ℂ) :
55     (tensor A).conjTranspose = tensor (fun i => (A i).conjTranspose) := by
56   ext x y
57   simp [tensor, Matrix.conjTranspose_apply]
58 end Tensor
59 
60 section Fine
61 variable {F : Type*} [Fintype F] [DecidableEq F] {D J : F → Type*}
62 variable [∀ i, Fintype (D i)] [∀ i, DecidableEq (D i)]
63 variable [∀ i, Fintype (J i)] [∀ i, DecidableEq (J i)]
64 variable (P : (i : F) → J i → Matrix (D i) (D i) ℂ)
65 
66 omit [∀ i, DecidableEq (D i)] [∀ i, Fintype (J i)] in
67 theorem fine_mul
68     (hmul : ∀ i j k, P i j * P i k = if j = k then P i j else 0)
69     (a b : (i : F) → J i) :
70     tensor (fun i => P i (a i)) * tensor (fun i => P i (b i)) =
71       if a = b then tensor (fun i => P i (a i)) else 0 := by
72   classical
73   rw [← tensor_mul]
74   by_cases h : a = b
75   · subst b
76     simp only [ite_true, hmul]
77   · simp only [h, ite_false]
78     obtain ⟨i, hi⟩ := Function.ne_iff.mp h
79     ext x y
80     simp only [tensor, Matrix.zero_apply]
81     apply Finset.prod_eq_zero (Finset.mem_univ i)
82     simp only [hmul, hi, ite_false]
83     rfl
84 
85 omit [∀ i, Fintype (D i)] [∀ i, DecidableEq (J i)] in
86 theorem fine_complete (hsum : ∀ i, ∑ j, P i j = 1) :
87     (∑ a : (i : F) → J i, tensor (fun i => P i (a i))) = 1 := by
88   rw [tensor_sum]
89   simp_rw [hsum]
90   exact tensor_one
91 
92 omit [DecidableEq F] [∀ i, Fintype (D i)] [∀ i, DecidableEq (D i)]
93   [∀ i, Fintype (J i)] [∀ i, DecidableEq (J i)] in
94 theorem fine_selfAdjoint (hstar : ∀ i j, (P i j).conjTranspose = P i j)
95     (a : (i : F) → J i) :
96     (tensor (fun i => P i (a i))).conjTranspose = tensor (fun i => P i (a i)) := by
97   rw [tensor_adjoint]
98   simp_rw [hstar]
99 end Fine
100 
101 section Coarse
102 variable {R I J : Type*} [Ring R] [Fintype I] [DecidableEq I]
103 variable [Fintype J] [DecidableEq J]
104 def coarse (P : I → R) (address : I → J) (r : J) : R :=
105   ∑ a, if address a = r then P a else 0
106 
107 omit [Fintype J] in
108 theorem coarse_mul (P : I → R) (address : I → J)
109     (hmul : ∀ a b, P a * P b = if a = b then P a else 0) (r s : J) :
110     coarse P address r * coarse P address s =
111       if r = s then coarse P address r else 0 := by
112   unfold coarse
113   simp only [Finset.sum_mul, Finset.mul_sum]
114   have term (a b : I) :
115       (if address a = r then P a else 0) * (if address b = s then P b else 0) =
116       if a = b then (if address a = r ∧ r = s then P a else 0) else 0 := by
117     by_cases hab : a = b
118     · subst b
119       by_cases hr : address a = r <;> by_cases hs : r = s <;>
120         simp_all
121     · simp [hmul, hab, ite_mul, mul_ite]
122   simp_rw [term]
123   by_cases hrs : r = s <;> simp [hrs]
124 
125 omit [DecidableEq I] in
126 theorem coarse_complete (P : I → R) (address : I → J) (hsum : ∑ a, P a = 1) :
127     (∑ r, coarse P address r) = 1 := by
128   unfold coarse
129   rw [Finset.sum_comm]
130   simpa using hsum
131 
132 omit [DecidableEq I] [Fintype J] in
133 theorem coarse_selfAdjoint [StarRing R] (P : I → R) (address : I → J)
134     (hstar : ∀ a, star (P a) = P a) (r : J) :
135     star (coarse P address r) = coarse P address r := by
136   simp [coarse, star_sum, apply_ite, hstar]
137 end Coarse
138 
139 theorem tensor_polyphase_refinement {F : Type*} [Fintype F] [DecidableEq F] {D : F → Type*}
140     [∀ i, Fintype (D i)] [∀ i, DecidableEq (D i)]
141     (N : ℕ) [NeZero N] (P : (i : F) → ZMod N → Matrix (D i) (D i) ℂ)
142     (hmul : ∀ i j k, P i j * P i k = if j = k then P i j else 0)
143     (hsum : ∀ i, ∑ j, P i j = 1)
144     (hstar : ∀ i j, (P i j).conjTranspose = P i j) :
145     let Q := fun a : F → ZMod N => tensor (fun i => P i (a i))
146     let C := coarse Q (fun a => ∑ i, a i)
147     (∀ r s, C r * C s = if r = s then C r else 0) ∧
148       (∑ r, C r) = 1 ∧ (∀ r, (C r).conjTranspose = C r) := by
149   classical
150   dsimp only
151   refine ⟨?_, ?_, ?_⟩
152   · exact coarse_mul _ _ (fine_mul P hmul)
153   · exact coarse_complete _ _ (fine_complete P hsum)
154   · exact coarse_selfAdjoint _ _ (fine_selfAdjoint P hstar)
155 end KomorebiPaperVII.TensorRefinement
156 
157 #print axioms KomorebiPaperVII.TensorRefinement.tensor_mul
158 #print axioms KomorebiPaperVII.TensorRefinement.tensor_one
159 #print axioms KomorebiPaperVII.TensorRefinement.tensor_sum
160 #print axioms KomorebiPaperVII.TensorRefinement.tensor_adjoint
161 #print axioms KomorebiPaperVII.TensorRefinement.fine_mul
162 #print axioms KomorebiPaperVII.TensorRefinement.fine_complete
163 #print axioms KomorebiPaperVII.TensorRefinement.fine_selfAdjoint
164 #print axioms KomorebiPaperVII.TensorRefinement.coarse_mul
165 #print axioms KomorebiPaperVII.TensorRefinement.coarse_complete
166 #print axioms KomorebiPaperVII.TensorRefinement.coarse_selfAdjoint
167 #print axioms KomorebiPaperVII.TensorRefinement.tensor_polyphase_refinement

Back to source controls