Update tensor.lean

Nevanlinna/tensor.lean

@@ -0,0 +1,47 @@
+import Mathlib.Analysis.InnerProductSpace.PiL2
+
+
+open RCLike Real Filter
+open Topology ComplexConjugate
+open LinearMap (BilinForm)
+open TensorProduct
+open InnerProductSpace
+open Inner
+
+
+example
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [InnerProductSpace ℝ F]
+  : 1 = 0 := by
+
+  let e : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := innerₗ E 
+  let f : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₗ F 
+  let e₂ :=  TensorProduct.map₂ e f
+  let l := TensorProduct.lid ℝ ℝ 
+
+  have : ∀ e1 e2 : E, ∀ f1 f2 : F, e₂ (e1 ⊗ f1) (e2 ⊗ f2) = 
+
+  let X : InnerProductSpace.Core ℝ (E ⊗[ℝ] F) := {
+    inner := by
+      intro a b
+      exact TensorProduct.lid ℝ ℝ ((TensorProduct.map₂ (innerₗ E) (innerₗ F)) a b)
+    conj_symm := by
+      simp
+      intro x y
+
+      unfold innerₗ
+      
+      simp
+      sorry
+    nonneg_re := _
+    definite := _
+    add_left := _
+    smul_left := _
+  }
+
+  let inner : E ⊗[𝕜] E → E ⊗[𝕜] E → 𝕜 := 
+    --let x := TensorProduct.lift
+    --E.inner
+    --TensorProduct.map₂
+    sorry
+  sorry