From 42cf2e41b961fd39ab75b41ea42cf2982b6398a6 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Mon, 24 Jun 2024 12:14:18 +0200
Subject: [PATCH] Update laplace2.lean

---
 Nevanlinna/laplace2.lean | 49 ++++++++++++++++++++++++----------------
 1 file changed, 29 insertions(+), 20 deletions(-)

diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
index c87fa76..6f4830d 100644
--- a/Nevanlinna/laplace2.lean
+++ b/Nevanlinna/laplace2.lean
@@ -3,6 +3,7 @@ import Mathlib.Analysis.InnerProductSpace.PiL2
 import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Analysis.Calculus.ContDiff.Bounds
 import Mathlib.Analysis.Calculus.FDeriv.Symmetric
+import Mathlib.LinearAlgebra.Basis
 
 open BigOperators
 open Finset
@@ -10,24 +11,19 @@ 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₂
+lemma vectorPresentation
   [Fintype ι]
-  (v : Basis ι ℝ E)
-  (hv : Orthonormal ℝ v)
-  (f : E → F) :
-  E → F :=
-  fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
+  (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
 
-#check ContinuousMultilinearMap.map_sum_finset
 
 theorem LaplaceIndep
   [Fintype ι]
@@ -54,12 +50,12 @@ theorem LaplaceIndep
     --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
+  --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
+  --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)
@@ -70,3 +66,16 @@ theorem LaplaceIndep
   simp at X
   
   sorry
+
+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]