test file

Author: goliath-klein

QCLib/Circuit/Gate/Qubit.lean

@@ -9,6 +9,7 @@ public import Mathlib.LinearAlgebra.Matrix.Hermitian
 public import QCLib.LinearAlgebra.UnitaryGroup.RootsOfUnity
 public import QCLib.LinearAlgebra.StdBasis
 public import QCLib.Misc.OrderOf
+public import Mathlib.Analysis.InnerProductSpace.PiL2
 
 import QCLib.Misc.IntCast
 
@@ -77,8 +78,7 @@ noncomputable def T : 𝐔[Qubit] :=
 
 noncomputable def R (k : ℕ) : 𝐔[Qubit] := ⟨!![1, 0; 0, ζ (2^k)], by
   rw [Matrix.mem_unitaryGroup_iff]
-  matrix_expand
-  ⟩
+  matrix_expand ⟩
 
 @[matrixExpand]
 theorem H_eq : H.val = (√(1/2) : ℂ) • !![1, 1; 1, -1] := by rfl
@@ -291,6 +291,8 @@ def mns : (Qubit → ℂ) := ((√2)⁻¹ : ℂ) • (δ[0] - δ[1])
 def lft : (Qubit → ℂ) := ((√2)⁻¹ : ℂ) • (δ[0] + I • δ[1])
 def rgt : (Qubit → ℂ) := ((√2)⁻¹ : ℂ) • (δ[0] - I • δ[1])
 
+def upl2 : EuclideanSpace
+
 end
 
 example : pls = (√2)⁻¹ • ![1, 1] := by matrix_expand [pls]

QCLib/LinearAlgebra/StdBasis.lean

@@ -38,6 +38,9 @@ This file also collects `•` application
 noncomputable def BasisVector {ι : Type*} [Finite ι] (i : ι) : (ι → ℂ) :=
   Pi.basisFun ℂ ι i
 
+noncomputable def l2BasisVector {ι : Type*} [Finite ι] (i : ι) : (ι → ℂ) :=
+  Pi.basisFun ℂ ι i
+
 @[matrixExpand]
 theorem basisVector_def (ι : Type*) [Finite ι] (i : ι) :
   BasisVector i = Pi.basisFun ℂ ι i := by rfl

QCLib/Mathlib/LinearAlgebra/EuclideanPi-testing.lean

@@ -0,0 +1,14 @@
+import Mathlib
+import QCLib.Mathlib.LinearAlgebra.PiOuterProduct
+
+open scoped PiOuterProduct
+
+variable {ι : Type*} [Fintype ι]
+
+variable {l : ι → Type*} [∀ i, Fintype (l i)]
+
+-- family of vectors in an Euclidean space
+variable {f : (i : ι) → EuclideanSpace ℂ (l i)}
+
+instance : PiOuterProduct (fun i ↦ EuclideanSpace ℂ (l i)) (EuclideanSpace ℂ (Π i, l i)) where
+  tprod := fun f ↦ WithLp.toLp 2 (⨂ i, ((f i) : (l i → ℂ)))