Skip to content

Commit 13881b1

Browse files
goliath-kleingoliath-klein
committed
some thoughts
1 parent d130e8e commit 13881b1

3 files changed

Lines changed: 250 additions & 2 deletions

File tree

‎QCLib/Circuit/Hadamard.lean‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -58,7 +58,10 @@ private theorem HH_aux (y : Fin 2) :
5858

5959
-- TBD: `simp` runs into a loop. Investigate.
6060
theorem HH_apply (k : Register n) : (HH n) • δ[k] = HadamardBasisVector n k := by
61-
simp_rw [HH_def, HadamardBasisVector, basisVector_eq_prod, piKroneckerUnitary_smul_vec, H_apply,
61+
simp_rw [HH_def, HadamardBasisVector, basisVector_eq_prod]
62+
-- simp_rw [piKroneckerUnitary_smul_vec]
63+
simp_rw [EuclideanSpace.piKroneckerUnitary_smul_vec]
64+
simp_rw [H_apply,
6265
piOuterProduct_smul_const, HH_aux, piOuterProduct_univ_sum, Fintype.card_fin,
6366
piOuterProduct_smul_univ, Finset.prod_pow_eq_pow_sum]
6467

‎QCLib/LinearAlgebra/StdBasis-dg-test.lean‎

Lines changed: 245 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,245 @@
1+
/-
2+
Copyright (c) 2026 Davood Tehrani, David Gross. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Davood Tehrani, David Gross
5+
-/
6+
module
7+
8+
public import Mathlib.Analysis.InnerProductSpace.PiL2
9+
public import QCLib.Mathlib.LinearAlgebra.PiOuterProduct
10+
public import QCLib.LinearAlgebra.UnitaryGroup.Basic
11+
12+
import QCLib.Tactic.MatrixExpand
13+
import QCLib.Mathlib.Lemmas
14+
15+
/-!
16+
# Bases
17+
18+
## Main definitions
19+
20+
* `BasisVector`, a synonym for `Pi.basisFun ℂ`
21+
* `Qubit` for `Fin 2`, so that the vector space for a single qubit is `Qubit → ℂ`
22+
* `Register n` for `(Fin n) → Qubit`, so that the vector space for `n` qubits is `Register n → ℂ`
23+
* `PiOuterPrdocutInst` A type class instance that provides outer product notation
24+
for dependent families of `EuclideanSpace` vectors.
25+
26+
## Main results
27+
28+
* `basisVector_eq_prod` standard basis functions factorize
29+
* `PiOuterProduct.toMultilinearMap` Outer products as multilinear maps.
30+
31+
This file also collects `•` application
32+
33+
## Notation
34+
35+
* `δ[i]` for `BasisVector i`
36+
37+
-/
38+
39+
-- creates a simp loop with `WithLp.zero_def`
40+
attribute [-simp] WithLp.toLp_zero
41+
42+
-- why aren't these set?
43+
attribute [coe] WithLp.ofLp
44+
attribute [norm_cast] WithLp.ofLp_smul
45+
46+
public section
47+
48+
/-
49+
Missing instance, which should go into the section around `WithLp.instNontrivial`.
50+
-/
51+
section WithLpMissingInstances
52+
53+
namespace WithLp
54+
55+
open scoped ENNReal
56+
57+
variable (p : ℝ≥0∞) (K K' : Type*) {K'' : Type*} (V : Type*) {V' V'' : Type*}
58+
59+
@[to_additive (attr := simps)]
60+
instance instOne [One V] : One (WithLp p V) := (WithLp.equiv p V).one
61+
62+
end WithLpMissingInstances.WithLp
63+
64+
section test
65+
66+
variable {ι : Type*} [Fintype ι]
67+
variable {α : Type*} [Zero α]
68+
69+
example (i : ι) : (0 : EuclideanSpace α ι) i = 0 := by
70+
simp_rw [WithLp.zero_def, WithLp.equiv_symm_apply, Pi.zero_apply]
71+
72+
example : (SubtractionMonoid.toSubNegZeroMonoid.toNegZeroClass.toZero.zero : (EuclideanSpace ℂ ι))
73+
= ((WithLp.instZero _ _).zero : (EuclideanSpace ℂ ι)) := by
74+
with_reducible_and_instances rfl
75+
76+
example (i : ι) : (0 : EuclideanSpace ℂ ι) i = 0 := by
77+
simp
78+
79+
end test
80+
81+
open EuclideanSpace PiOuterProduct Function
82+
83+
variable {ι : Type*} [Fintype ι]
84+
85+
namespace EuclideanSpace
86+
87+
variable {α : Type*} (l : ι → Type*)
88+
89+
theorem ext {α n : Type*} {x y : EuclideanSpace α n} (h : x.ofLp = y.ofLp) : x = y :=
90+
WithLp.ofLp_injective 2 h
91+
92+
@[simp]
93+
theorem ofLp_update_apply {ι : Type*} [DecidableEq ι] {l : ι → Type*}
94+
(f : Π i, EuclideanSpace α (l i)) (i' : ι) (x : EuclideanSpace α (l i'))
95+
(j : Π i, l i) (i : ι) :
96+
(update f i' x i).ofLp (j i)
97+
= update (fun i ↦ (f i).ofLp (j i)) i' (x.ofLp (j i')) i :=
98+
apply_update (fun i (v : EuclideanSpace α (l i)) ↦ v.ofLp (j i)) f i' x i
99+
100+
instance instPiOuterProduct [CommMonoid α] :
101+
PiOuterProduct (fun i ↦ EuclideanSpace α (l i)) (EuclideanSpace α (Π i, l i)) where
102+
tprod f := WithLp.toLp 2 (⨂ i, ((f i) : (l i → α)))
103+
104+
@[simp, norm_cast]
105+
theorem ofLp_injective [CommMonoid α] (f : Π i, EuclideanSpace α (l i)) :
106+
(⨂ i, f i).ofLp = (⨂ i, (f i).ofLp) := rfl
107+
108+
example [CommMonoid α] (f : (i : ι) → EuclideanSpace α (l i)) (j) :
109+
(⨂ i, f i) j = ∏ i, f i (j i) := by simp
110+
111+
-- remove? geometrically, the all-ones vector isn't distinguished in an l2 space.
112+
@[simp]
113+
theorem piOuterProduct_one [CommMonoid α] :
114+
(⨂ i, (WithLp.toLp 2 (1 : l i → α) : EuclideanSpace α (l i)))
115+
= (WithLp.toLp 2 (1 : (Π i, l i) → α) : EuclideanSpace α (Π i, l i)) := by
116+
apply ext
117+
simp
118+
119+
@[simp]
120+
theorem piOuterProduct_zero [CommMonoidWithZero α] (f : Π i, EuclideanSpace α (l i))
121+
(h : ∃ i, f i = 0) : (⨂ i, f i) = 0 := by
122+
ext j
123+
obtain ⟨i, hi⟩ := h
124+
simpa using Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi])
125+
126+
@[simp]
127+
theorem piOuterProduct_smul [CommSemiring α] [DecidableEq ι]
128+
(f : Π i, EuclideanSpace α (l i)) (i : ι) (s : α) (x : EuclideanSpace α (l i)) :
129+
(⨂ j, (update f i (s • x)) j) = s • (⨂ j, (update f i x) j) := by
130+
ext
131+
simp [Finset.prod_update_of_mem, mul_assoc]
132+
133+
-- Lean only synthesizes `Add` under `SeminormedAddCommGroup` assumption.
134+
-- See `PiLp.add_apply`. TBD: Investigate.
135+
@[simp]
136+
theorem piOuterProduct_add [DecidableEq ι] [CommMonoid α]
137+
[SeminormedAddCommGroup α] [RightDistribClass α]
138+
(f : Π i, EuclideanSpace α (l i)) (i : ι) (x y : EuclideanSpace α (l i)) :
139+
(⨂ j, (update f i (x + y)) j) = (⨂ j, (update f i x) j) + (⨂ j, (update f i y) j) := by
140+
ext
141+
simp [Finset.prod_update_of_mem, add_mul]
142+
143+
@[simps, expose]
144+
def PiOuterProduct.toMultilinearMap [SeminormedCommRing α] :
145+
MultilinearMap α (fun i ↦ EuclideanSpace α (l i)) (EuclideanSpace α (Π i, l i)) where
146+
toFun f := ⨂ i, f i
147+
map_update_add' := by simp
148+
map_update_smul' := by simp
149+
150+
theorem piOuterProduct_smul_univ [SeminormedCommRing α] (c : ι → α)
151+
(f : Π i, EuclideanSpace α (l i)) :
152+
(⨂ i, c i • f i) = (∏ i, c i) • (⨂ i, f i) := by
153+
apply ext
154+
simp [_root_.piOuterProduct_smul_univ]
155+
156+
theorem piOuterProduct_smul_const [SeminormedCommRing α] (a : α)
157+
(f : Π i, EuclideanSpace α (l i)) :
158+
(⨂ i, a • f i) = a ^ (Fintype.card ι) • (⨂ i, f i) := by
159+
apply ext
160+
simp [_root_.piOuterProduct_smul_const]
161+
162+
theorem piOuterProduct_univ_sum [DecidableEq ι] [SeminormedCommRing α] {κ : Type*} [Fintype κ]
163+
(g : (i : ι) → κ → EuclideanSpace α (l i)) :
164+
(⨂ i, ∑ j : κ, g i j) = ∑ k : (ι → κ), ⨂ i, g i (k i) := by
165+
apply ext
166+
simp [_root_.piOuterProduct_univ_sum]
167+
168+
end EuclideanSpace
169+
170+
noncomputable def BasisVector (i : ι) :=
171+
basisFun ι ℂ i
172+
173+
@[matrixExpand]
174+
theorem basisVector_def (i : ι) :
175+
BasisVector i = basisFun ι ℂ i := by rfl
176+
177+
-- TBD: scope
178+
/-- The computational basis. -/
179+
notation3:max "δ[" i:90 "] " => BasisVector i
180+
181+
-- `ext` lemma stated for `SMul` action of unitaries on vectors.
182+
-- TBD: Get rid of this? Formulate in terms of `toLin` and general Bases? State
183+
-- for `MatrixLike` objects?
184+
-- More generally, decide whether to use `•` for actions on vectors
185+
-- Move to other module?
186+
theorem Matrix.UnitaryGroup.ext_col [DecidableEq ι]
187+
{U V : Matrix.unitaryGroup ι ℂ} :
188+
(∀ i : ι, (U : Matrix ι ι ℂ).col i = (V : Matrix ι ι ℂ).col i) → U = V := by
189+
intro h
190+
apply Subtype.ext
191+
exact Matrix.ext_col h
192+
193+
variable [DecidableEq ι]
194+
195+
open Matrix in
196+
theorem Matrix.unitaryGroup.smul_euclidean_vec_def
197+
{α m : Type*} [Fintype m] [DecidableEq m] [CommRing α] [StarRing α]
198+
(U : unitaryGroup m α) (v : EuclideanSpace α m) : U • v = WithLp.toLp 2 (↑U *ᵥ v.ofLp) := by
199+
ext
200+
simp [Submonoid.smul_def]
201+
202+
open Matrix in
203+
@[simp]
204+
theorem Matrix.unitaryGroup.smul_euclidean_vec_coe
205+
{α m : Type*} [Fintype m] [DecidableEq m] [CommRing α] [StarRing α]
206+
(U : unitaryGroup m α) (v : EuclideanSpace α m) : ((U • v) : m → α) = (↑U *ᵥ v.ofLp) := by
207+
ext
208+
simp [Submonoid.smul_def]
209+
210+
theorem Matrix.UnitaryGroup.ext_smul_basis
211+
{U V : Matrix.unitaryGroup ι ℂ} : (∀ i : ι, (U • δ[i]) = V • δ[i]) → U = V := by
212+
simpa [basisVector_def, Matrix.unitaryGroup.smul_euclidean_vec_def] using ext_col
213+
214+
@[simp]
215+
theorem Matrix.UnitaryGroup.diagonal_smul_basisVector
216+
(d : ι → unitary ℂ) (i : ι) : (diagonalMonoidHom d) • δ[i] = (d i) • δ[i] := by
217+
ext j
218+
simp [Submonoid.smul_def, basisVector_def, Pi.single_apply]
219+
220+
@[simp]
221+
theorem Matrix.diagonal_smul_basisVector (d : ι → ℂ) (v : ι) :
222+
Matrix.diagonal d • δ[v] = d v • δ[v] := by
223+
ext i
224+
simp [basisVector_def, basisFun_apply, Pi.single_apply]
225+
226+
theorem Matrix.UnitaryGroup.apply_basis {U : Matrix.unitaryGroup ι ℂ} (v : ι) :
227+
U • δ[v] = ∑ i, U i v • δ[i] := by
228+
ext
229+
simp [basisVector_def, Pi.single_apply, Submonoid.smul_def]
230+
231+
section SMul
232+
233+
section Qubits
234+
235+
abbrev Qubit := Fin 2
236+
abbrev Register (n : Nat) := (Fin n) → Qubit
237+
238+
open Complex Matrix
239+
open scoped PiOuterProduct
240+
241+
theorem basisVector_eq_prod {d} {n : ℕ} (k : Fin n → Fin d) : δ[k] = ⨂ i, δ[(k i)] := by
242+
ext
243+
simp [basisVector_def, ← Pi.single_eq_prod, ← Pi.single_apply]
244+
245+
end Qubits

‎QCLib/Mathlib/LinearAlgebra/PiOuterProduct.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -136,7 +136,7 @@ theorem piOuterProduct_apply [CommMonoid α] (v : Π i, (l i → α)) (r : Π i,
136136
simp [piOuterProduct_def, ← Multiset.prod_eq_foldr]
137137

138138
@[simp]
139-
theorem piOuterProduct_one [CommMonoidWithZero α] : (⨂ i, (1 : m i → α)) = 1 := by ext; simp
139+
theorem piOuterProduct_one [CommMonoid α] : (⨂ i, (1 : m i → α)) = 1 := by ext; simp
140140

141141
@[simp]
142142
theorem piOuterProduct_zero [CommMonoidWithZero α] (v : Π i, (l i → α)) (h : ∃ i, v i = 0) :

0 commit comments

Comments
 (0)