Create bilinear.lean

Nevanlinna/bilinear.lean

@@ -0,0 +1,39 @@
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.InnerProductSpace.Dual
+import Mathlib.Analysis.InnerProductSpace.PiL2
+
+
+open BigOperators
+open Finset
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+open TensorProduct
+
+example : 0 = 1 := by
+
+  let B := (sesqFormOfInner (𝕜 := ℝ) (E := E)).flip
+
+
+  have e: E := by sorry
+  let C := B e
+
+  let α :=  InnerProductSpace.toDual ℝ E
+
+  let β : E →ₗ[ℝ] ℝ := by sorry
+  let YY := E ⊗[ℝ] E
+
+  let ZZ := TensorProduct.mapBilinear ℝ E E ℝ ℝ
+
+
+  let A : E × E → LinearMap.BilinForm ℝ E := by
+    unfold LinearMap.BilinForm
+    intro (e₁, e₂)
+
+
+
+    sorry
+
+  sorry