diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean
index 7f6f5fe..54869fc 100644
--- a/Nevanlinna/bilinear.lean
+++ b/Nevanlinna/bilinear.lean
@@ -1,4 +1,4 @@
-import Mathlib.Algebra.BigOperators.Basic
+--import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.PiL2
@@ -9,31 +9,164 @@ 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₂)
+open BigOperators
+open Finset
 
 
 
-    sorry
+lemma vectorPresentation
+  [Fintype ι]
+  (b : Basis ι ℝ E)
+  (hb : Orthonormal ℝ b)
+  (v : E) :
+  v = ∑ i, ⟪b i, v⟫_ℝ • (b i) := by
+  nth_rw 1 [← (b.sum_repr v)] 
+  apply Fintype.sum_congr
+  intro i
+  rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
+  simp
+
+
+theorem BilinearCalc
+  [Fintype ι]
+  (v : Basis ι ℝ E)
+  (c : ι → ℝ)
+  (L : E →ₗ[ℝ] E →ₗ[ℝ] F) 
+  : L (∑ j : ι, c j • v j) (∑ j : ι, c j • v j) 
+    = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L (v (x 0)) (v (x 1)) := by
+  
+  rw [map_sum]
+  rw [map_sum]
+
+  conv =>
+    left
+    arg 2
+    intro r
+    rw [← sum_apply]
+
+    rw [map_smul]
+    arg 2
+    arg 1
+    arg 2
+    intro x
+    rw [map_smul]
+  simp
+
+
+lemma c2
+  [Fintype ι]
+  (b : Basis ι ℝ E)
+  (hb : Orthonormal ℝ b)
+  (x y : E) :
+  ⟪x, y⟫_ℝ = ∑ i : ι, ⟪x, b i⟫_ℝ * ⟪y, b i⟫_ℝ := by
+  rw [vectorPresentation b hb x]
+  rw [vectorPresentation b hb y]
+  rw [Orthonormal.inner_sum hb]
+  simp
+  conv =>
+    right
+    arg 2
+    intro i'
+    rw [Orthonormal.inner_left_fintype hb]
+    rw [Orthonormal.inner_left_fintype hb]
+
+
+lemma fin_sum
+  [Fintype ι]
+  (f : ι → ι → F) :
+  ∑ r : Fin 2 → ι, f (r 0) (r 1) = ∑ r₀ : ι, (∑ r₁ : ι, f r₀ r₁) := by
+
+  rw [← Fintype.sum_prod_type']
+  apply Fintype.sum_equiv (finTwoArrowEquiv ι)
+  intro x
+  dsimp 
+
+theorem TensorIndep
+  [Fintype ι] [DecidableEq ι]
+  (v₁ : Basis ι ℝ E)
+  (hv₁ : Orthonormal ℝ v₁)
+  (v₂ : Basis ι ℝ E)
+  (hv₂ : Orthonormal ℝ v₂) :
+  ∑ i, (v₁ i) ⊗ₜ[ℝ] (v₁ i) = ∑ i, (v₂ i) ⊗ₜ[ℝ] (v₂ i) := by
+
+  conv =>
+    right
+    arg 2
+    intro i
+    rw [vectorPresentation v₁ hv₁ (v₂ i)]
+    rw [TensorProduct.sum_tmul]
+    arg 2
+    intro j
+    rw [TensorProduct.tmul_sum]
+    arg 2
+    intro a
+    rw [TensorProduct.tmul_smul]
+    arg 2
+    rw [TensorProduct.smul_tmul]
+
+  rw [Finset.sum_comm]
+  conv =>
+    right
+    arg 2
+    intro i
+    rw [Finset.sum_comm]
+
+
 
   sorry
+
+theorem LaplaceIndep
+  [Fintype ι] [DecidableEq ι]
+  (v₁ : Basis ι ℝ E)
+  (hv₁ : Orthonormal ℝ v₁)
+  (v₂ : Basis ι ℝ E)
+  (hv₂ : Orthonormal ℝ v₂)
+  (L : E →ₗ[ℝ] E →ₗ[ℝ] F) :
+  ∑ i, L (v₁ i) (v₁ i) = ∑ i, L (v₂ i) (v₂ i) := by
+
+  have vector_vs_function
+    {y : Fin 2 → ι} 
+    {v : ι → E}
+    : (fun i => v (y i)) = ![v (y 0), v (y 1)] := by 
+    funext i
+    by_cases h : i = 0
+    · rw [h]
+      simp
+    · rw [Fin.eq_one_of_neq_zero i h]
+      simp
+
+  conv =>
+    right
+    arg 2
+    intro i
+    rw [vectorPresentation v₁ hv₁ (v₂ i)]
+    rw [BilinearCalc]
+  rw [Finset.sum_comm]
+  conv =>
+    right
+    arg 2
+    intro y
+    rw [← Finset.sum_smul]
+    rw [← c2 v₂ hv₂ (v₁ (y 0)) (v₁ (y 1))]
+    rw [vector_vs_function]
+  simp
+
+  rw [fin_sum (fun i₀ ↦ (fun i₁ ↦ ⟪v₁ i₀, v₁ i₁⟫_ℝ • L ![v₁ i₀, v₁ i₁]))]
+    
+  have xx {r₀ : ι} : ∀ r₁ : ι, r₁ ≠ r₀ → ⟪v₁ r₀, v₁ r₁⟫_ℝ • L ![v₁ r₀, v₁ r₁] = 0 := by
+    intro r₁ hr₁
+    rw [orthonormal_iff_ite.1 hv₁]
+    simp
+    tauto
+
+  conv =>
+    right
+    arg 2
+    intro r₀
+    rw [Fintype.sum_eq_single r₀ xx]
+    rw [orthonormal_iff_ite.1 hv₁]
+  apply sum_congr
+  rfl
+  intro x _
+  rw [vector_vs_function]
+  simp
diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
index 7597bac..cdc5023 100644
--- a/Nevanlinna/laplace2.lean
+++ b/Nevanlinna/laplace2.lean
@@ -1,7 +1,7 @@
 import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Analysis.InnerProductSpace.Dual
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import Mathlib.Algebra.BigOperators.Basic
+--import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Bounds
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
 import Mathlib.LinearAlgebra.Basis
diff --git a/lake-manifest.json b/lake-manifest.json
index 2f2d2de..bbb73cc 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -31,10 +31,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.38",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "9c4c6f78c9a1b7beba018504e284d497a3761af2",
+   "rev": "dcc73cfb2ce3763f830c52042fb8617e762dbf60",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,