diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean new file mode 100644 index 0000000..7f6f5fe --- /dev/null +++ b/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