New file

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