ComputationalSeed.lean

1 module
2 public import Mathlib.LinearAlgebra.StdBasis
3 public import Mathlib.Data.ZMod.Basic
4 public import Mathlib.Data.Fintype.Pi
5 public import Mathlib.Data.List.OfFn
6 public import Mathlib.Algebra.BigOperators.Fin
7 public import Mathlib.Analysis.Complex.Basic
8 public import Mathlib.Tactic.FinCases
9 /-! Author: Komorebi P. Paper VII second block, Theorem 2.4.
10 A composition of addressed local X gates generates the full computational basis. -/
11 public section
12 set_option autoImplicit false
13 namespace KomorebiPaperVII.ComputationalSeed
14 open scoped BigOperators
15 abbrev Address (n : ℕ) := Fin n → ZMod 2
16 abbrev State (n : ℕ) := Address n → ℂ
17 def ket {n : ℕ} (a : Address n) : State n := Pi.single a 1
18 def seed (n : ℕ) : State n := ket 0
19 def translation {n : ℕ} (a : Address n) : Module.End ℂ (State n) where
20   toFun := fun v x => v (x - a)
21   map_add' := by intros; rfl
22   map_smul' := by intros; rfl
23 
24 theorem translation_zero (n : ℕ) : translation (0 : Address n) = 1 := by
25   ext v x
26   simp [translation]
27 theorem translation_add {n : ℕ} (a b : Address n) :
28     translation a * translation b = translation (a + b) := by
29   ext v x
30   simp [translation, sub_sub]
31 theorem translation_ket {n : ℕ} (a b : Address n) :
32     translation a (ket b) = ket (a + b) := by
33   ext x
34   simp [translation, ket, Pi.single_apply, sub_eq_iff_eq_add, add_comm]
35 theorem translation_involution {n : ℕ} (a : Address n) :
36     translation a * translation a = 1 := by
37   rw [translation_add, ZModModule.add_self, translation_zero]
38 def bit {n : ℕ} (j : Fin n) : Address n := Pi.single j 1
39 def localX {n : ℕ} (j : Fin n) : Module.End ℂ (State n) := translation (bit j)
40 theorem localX_on_ket {n : ℕ} (j : Fin n) (a : Address n) :
41     localX j (ket a) = ket (Function.update a j (a j + 1)) := by
42   rw [localX, translation_ket]
43   congr 1
44   ext k
45   by_cases hk : k = j
46   · subst k
47     simp [bit, add_comm]
48   · simp [bit, hk]
49 def controlledX {n : ℕ} (a : Address n) (j : Fin n) : Module.End ℂ (State n) :=
50   if a j = 0 then 1 else localX j
51 theorem controlledX_eq_translation {n : ℕ} (a : Address n) (j : Fin n) :
52     controlledX a j = translation (Pi.single j (a j)) := by
53   have h : a j = 0 ∨ a j = 1 := by
54     generalize a j = b
55     fin_cases b
56     · exact Or.inl rfl
57     · exact Or.inr rfl
58   rcases h with h | h
59   · simp [controlledX, h, translation_zero]
60   · simp [controlledX, h, localX, bit]
61 def addressCircuit {n : ℕ} (a : Address n) : Module.End ℂ (State n) :=
62   (List.ofFn (fun j : Fin n => controlledX a j)).prod
63 theorem translation_list_product {n : ℕ} (L : List (Address n)) :
64     (L.map translation).prod = translation L.sum := by
65   induction L with
66   | nil => simp [translation_zero]
67   | cons a L ih => simp only [List.map_cons, List.prod_cons, List.sum_cons, ih, translation_add]
68 theorem sum_local_addresses {n : ℕ} (a : Address n) :
69     (∑ j, Pi.single j (a j)) = a := by
70   ext k
71   simp [Finset.sum_apply, Pi.single_apply]
72 theorem circuit_eq_translation {n : ℕ} (a : Address n) :
73     addressCircuit a = translation a := by
74   unfold addressCircuit
75   simp_rw [controlledX_eq_translation]
76   simpa only [List.map_ofFn, Function.comp_def, List.sum_ofFn, sum_local_addresses] using
77     translation_list_product (List.ofFn (fun j : Fin n => Pi.single j (a j)))
78 theorem circuit_seed {n : ℕ} (a : Address n) : addressCircuit a (seed n) = ket a := by
79   rw [circuit_eq_translation, seed, translation_ket, add_zero]
80 theorem circuit_seed_basis {n : ℕ} (a : Address n) :
81     addressCircuit a (seed n) = Pi.basisFun ℂ (Address n) a := by
82   rw [circuit_seed, Pi.basisFun_apply, ket]
83 theorem addressed_seed_linearIndependent (n : ℕ) :
84     LinearIndependent ℂ (fun a : Address n => addressCircuit a (seed n)) := by
85   simp_rw [circuit_seed_basis]
86   exact (Pi.basisFun ℂ (Address n)).linearIndependent
87 theorem addressed_seed_spans (n : ℕ) :
88     Submodule.span ℂ (Set.range (fun a : Address n => addressCircuit a (seed n))) = ⊤ := by
89   simp_rw [circuit_seed_basis]
90   exact (Pi.basisFun ℂ (Address n)).span_eq
91 theorem number_of_addresses (n : ℕ) : Fintype.card (Address n) = 2 ^ n := by
92   simp [Address]
93 end KomorebiPaperVII.ComputationalSeed
94 
95 #print axioms KomorebiPaperVII.ComputationalSeed.translation_zero
96 #print axioms KomorebiPaperVII.ComputationalSeed.translation_add
97 #print axioms KomorebiPaperVII.ComputationalSeed.translation_ket
98 #print axioms KomorebiPaperVII.ComputationalSeed.translation_involution
99 #print axioms KomorebiPaperVII.ComputationalSeed.localX_on_ket
100 #print axioms KomorebiPaperVII.ComputationalSeed.controlledX_eq_translation
101 #print axioms KomorebiPaperVII.ComputationalSeed.translation_list_product
102 #print axioms KomorebiPaperVII.ComputationalSeed.sum_local_addresses
103 #print axioms KomorebiPaperVII.ComputationalSeed.circuit_eq_translation
104 #print axioms KomorebiPaperVII.ComputationalSeed.circuit_seed
105 #print axioms KomorebiPaperVII.ComputationalSeed.circuit_seed_basis
106 #print axioms KomorebiPaperVII.ComputationalSeed.addressed_seed_linearIndependent
107 #print axioms KomorebiPaperVII.ComputationalSeed.addressed_seed_spans
108 #print axioms KomorebiPaperVII.ComputationalSeed.number_of_addresses

Back to source controls