From adc0378e5db644f76690ee560a1f5e7537346853 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 24 Jun 2024 07:58:04 +0200
Subject: [PATCH] Update laplace2.lean

---
 Nevanlinna/laplace2.lean | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
index b6cee8b..f36cb58 100644
--- a/Nevanlinna/laplace2.lean
+++ b/Nevanlinna/laplace2.lean
@@ -27,6 +27,8 @@ 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)
@@ -49,5 +51,20 @@ 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_finset 
+    (iteratedFDeriv ℝ 2 f z)
+    (fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j)))
+    (fun _ ↦ Finset.univ)
+  simp at X
+  
   sorry