Nevanlinna/laplace2.lean

@@ -27,8 +27,6 @@ noncomputable def Laplace₂
   E → F :=
   fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
 
-#check ContinuousMultilinearMap.map_sum_finset
-
 theorem LaplaceIndep
   [Fintype ι]
   (v₁ : Basis ι ℝ E)
@@ -51,22 +49,5 @@ theorem LaplaceIndep
     right
     arg 2
     intro i
-    --rw [ContinuousMultilinearMap.map_sum_finset]
+    rw [ContinuousMultilinearMap.map_sum_finset]
-
-  have v : E := by sorry
-  let t := ![∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j), ∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j)]
-  simp at t
-  have L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F := by exact iteratedFDeriv ℝ 2 f z
-  --have α : Fin 2 → Type* := by exact fun _ ↦ ι
-  have g : (i : Fin 2) → ι → E := by exact fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j))
-  have A : (i : Fin 2) → Finset ι := by exact fun _ ↦ Finset.univ
-
-  let X := ContinuousMultilinearMap.map_sum
-    (iteratedFDeriv ℝ 2 f z)
-    (fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j)))
-
-  --
-  --  (fun _ ↦ Finset.univ)
-  simp at X
-  
   sorry