Pi namespace

Author: PrParadoxy

QCLib/Circuit/Hadamard.lean

@@ -29,7 +29,7 @@ a.k.a. the Hadamard basis.
 
 @[expose] public section
 
-open Qubit Matrix
+open Qubit Matrix EuclideanSpace
 open scoped PiOuterProduct
 
 variable (n : ℕ)

QCLib/LinearAlgebra/StdBasis-dg-test.lean

@@ -36,8 +36,31 @@ This file also collects `•` application
 
 -/
 
+-- creates a simp loop with `WithLp.zero_def`
+attribute [-simp] WithLp.toLp_zero
+
+-- why aren't these set?
+attribute [coe] WithLp.ofLp
+attribute [norm_cast] WithLp.ofLp_smul
+
 public section
 
+/-
+Missing instance, which should go into the section around `WithLp.instNontrivial`.
+-/
+section WithLpMissingInstances
+
+namespace WithLp
+
+open scoped ENNReal
+
+variable (p : ℝ≥0∞) (K K' : Type*) {K'' : Type*} (V : Type*) {V' V'' : Type*}
+
+@[to_additive (attr := simps)]
+instance instOne [One V] : One (WithLp p V) := (WithLp.equiv p V).one
+
+end WithLpMissingInstances.WithLp
+
 open EuclideanSpace PiOuterProduct Function
 
 variable {ι : Type*} [Fintype ι]
@@ -46,6 +69,10 @@ namespace EuclideanSpace
 
 variable {α : Type*} (l : ι → Type*)
 
+@[ext]
+theorem ext {α n : Type*} {x y : EuclideanSpace α n} (h : x.ofLp = y.ofLp) : x = y :=
+  WithLp.ofLp_injective 2 h
+
 @[simp]
 theorem ofLp_update_apply {ι : Type*} [DecidableEq ι] {l : ι → Type*}
     (f : Π i, EuclideanSpace α (l i)) (i' : ι) (x : EuclideanSpace α (l i'))
@@ -54,41 +81,39 @@ theorem ofLp_update_apply {ι : Type*} [DecidableEq ι] {l : ι → Type*}
       = update (fun i ↦ (f i).ofLp (j i)) i' (x.ofLp (j i')) i :=
   apply_update (fun i (v : EuclideanSpace α (l i)) ↦ v.ofLp (j i)) f i' x i
 
-instance PiOuterPrdocutInst [CommMonoid α] :
-    PiOuterProduct (fun i => EuclideanSpace α (l i)) (EuclideanSpace α (Π i, l i)) where
+instance instPiOuterProduct [CommMonoid α] :
+    PiOuterProduct (fun i ↦ EuclideanSpace α (l i)) (EuclideanSpace α (Π i, l i)) where
   tprod f := WithLp.toLp 2 (⨂ i, ((f i) : (l i → α)))
 
-@[simp]
-theorem piOuterProduct_apply [CommMonoid α] (f : (i : ι) → EuclideanSpace α (l i)) (j) :
-    (⨂ i, f i).ofLp j = ∏ i, f i (j i) := by
-  simp [PiOuterProduct.tprod, ← Multiset.prod_eq_foldr]
+@[simp, norm_cast]
+theorem ofLp_injective [CommMonoid α] (f : Π i, EuclideanSpace α (l i)) :
+    (⨂ i, f i).ofLp = (⨂ i, (f i).ofLp) := rfl
+
+example [CommMonoid α] (f : (i : ι) → EuclideanSpace α (l i)) (j) :
+    (⨂ i, f i) j = ∏ i, f i (j i) := by simp
 
+-- remove? geometrically, the all-ones vector isn't distinguished in an l2 space.
 @[simp]
-theorem piOuterProduct_one [CommMonoid α] :
-    (⨂ i, (WithLp.toLp 2 (1 : l i → α) : EuclideanSpace α (l i)))
-      = (WithLp.toLp 2 (1 : (Π i, l i) → α) : EuclideanSpace α (Π i, l i)) := by
-  ext j
+theorem piOuterProduct_one [CommMonoid α] : (⨂ i, (1 : EuclideanSpace α (l i))) = 1 := by
+  ext1
   simp
 
 @[simp]
 theorem piOuterProduct_zero [CommMonoidWithZero α] (f : Π i, EuclideanSpace α (l i))
-    (h : ∃ i, f i = (WithLp.toLp 2 (0 : l i → α) : EuclideanSpace α (l i))) :
-    (⨂ i, f i) = (WithLp.toLp 2 (0 : (Π i, l i) → α) : EuclideanSpace α (Π i, l i)) := by
+    (h : ∃ i, f i = 0) : (⨂ i, f i) = 0 := by
   ext j
   obtain ⟨i, hi⟩ := h
-  rw [piOuterProduct_apply]
-  exact Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi])
+  simpa using Finset.prod_eq_zero (Finset.mem_univ i) (by simp [hi])
 
 @[simp]
 theorem piOuterProduct_smul [CommSemiring α] [DecidableEq ι]
-    (f : Π i, EuclideanSpace α (l i)) (i : ι) (s : α)
-    (x : EuclideanSpace α (l i)) :
+    (f : Π i, EuclideanSpace α (l i)) (i : ι) (s : α) (x : EuclideanSpace α (l i)) :
     (⨂ j, (update f i (s • x)) j) = s • (⨂ j, (update f i x) j) := by
   ext
   simp [Finset.prod_update_of_mem, mul_assoc]
 
 -- Lean only synthesizes `Add` under `SeminormedAddCommGroup` assumption.
--- See `PiLp.add_apply`. Investigate why?
+-- See `PiLp.add_apply`. TBD: Investigate.
 @[simp]
 theorem piOuterProduct_add [DecidableEq ι] [CommMonoid α]
     [SeminormedAddCommGroup α] [RightDistribClass α]
@@ -99,26 +124,28 @@ theorem piOuterProduct_add [DecidableEq ι] [CommMonoid α]
 
 @[simps, expose]
 def PiOuterProduct.toMultilinearMap [SeminormedCommRing α] :
-    MultilinearMap α (fun i => EuclideanSpace α (l i)) (EuclideanSpace α (Π i, l i)) where
+    MultilinearMap α (fun i ↦ EuclideanSpace α (l i)) (EuclideanSpace α (Π i, l i)) where
   toFun f := ⨂ i, f i
   map_update_add' := by simp
   map_update_smul' := by simp
 
 theorem piOuterProduct_smul_univ [SeminormedCommRing α] (c : ι → α)
     (f : Π i, EuclideanSpace α (l i)) :
     (⨂ i, c i • f i) = (∏ i, c i) • (⨂ i, f i) := by
-  simp [← EuclideanSpace.PiOuterProduct.toMultilinearMap_apply, MultilinearMap.map_smul_univ]
+  ext1
+  simp [Pi.piOuterProduct_smul_univ]
 
 theorem piOuterProduct_smul_const [SeminormedCommRing α] (a : α)
     (f : Π i, EuclideanSpace α (l i)) :
     (⨂ i, a • f i) = a ^ (Fintype.card ι) • (⨂ i, f i) := by
-  simp [piOuterProduct_smul_univ]
+  ext1
+  simp [Pi.piOuterProduct_smul_const]
 
 theorem piOuterProduct_univ_sum [DecidableEq ι] [SeminormedCommRing α] {κ : Type*} [Fintype κ]
     (g : (i : ι) → κ → EuclideanSpace α (l i)) :
     (⨂ i, ∑ j : κ, g i j) = ∑ k : (ι → κ), ⨂ i, g i (k i) := by
-  ext x
-  simp [piOuterProduct_apply, Fintype.prod_sum]
+  ext1
+  simp [Pi.piOuterProduct_univ_sum]
 
 end EuclideanSpace