From d287c24453fa6808dc88ac03037f17bbe1448587 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sun, 23 Jun 2024 21:13:01 +0200
Subject: [PATCH] New file

---
 Nevanlinna/laplace2.lean | 53 ++++++++++++++++++++++++++++++++++++++++
 1 file changed, 53 insertions(+)
 create mode 100644 Nevanlinna/laplace2.lean

diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
new file mode 100644
index 0000000..b6cee8b
--- /dev/null
+++ b/Nevanlinna/laplace2.lean
@@ -0,0 +1,53 @@
+import Mathlib.Analysis.InnerProductSpace.Basic
+import Mathlib.Analysis.InnerProductSpace.PiL2
+import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Analysis.Calculus.ContDiff.Bounds
+import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+
+open BigOperators
+open Finset
+
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+
+#check EuclideanSpace.norm_eq
+#check EuclideanSpace.dist_eq
+
+
+noncomputable def Laplace₁ (n : ℕ) (f : EuclideanSpace ℝ (Fin n) → F) : EuclideanSpace ℝ (Fin n) → F := by
+  let e : Fin n → EuclideanSpace ℝ (Fin n) := fun i ↦ EuclideanSpace.single i (1 : ℝ)
+  exact fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![e i, e i]
+
+
+noncomputable def Laplace₂
+  [Fintype ι]
+  (v : Basis ι ℝ E)
+  (hv : Orthonormal ℝ v)
+  (f : E → F) :
+  E → F :=
+  fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
+
+theorem LaplaceIndep
+  [Fintype ι]
+  (v₁ : Basis ι ℝ E)
+  (hv₁ : Orthonormal ℝ v₁)
+  (v₂ : Basis ι ℝ E)
+  (hv₂ : Orthonormal ℝ v₂)
+  (f : E → F) :
+  ∑ i, iteratedFDeriv ℝ 2 f z ![v₁ i, v₁ i] =   ∑ i, iteratedFDeriv ℝ 2 f z ![v₂ i, v₂ i] := by
+
+  have (v : E) : v = ∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j) :=
+    sorry
+
+  conv =>
+    right
+    arg 2
+    intro i
+    rw [this (v₂ i)]
+    rw [this (v₂ i)]
+  conv =>
+    right
+    arg 2
+    intro i
+    rw [ContinuousMultilinearMap.map_sum_finset]
+  sorry