From c59e12a4680183ed4c5cbaa355b13183d34f0fc7 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 27 Jun 2024 06:35:02 +0200
Subject: [PATCH] Update laplace2.lean

---
 Nevanlinna/laplace2.lean | 53 ++++++++++++++++++++++++++++------------
 1 file changed, 37 insertions(+), 16 deletions(-)

diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
index b8d8388..dc787ef 100644
--- a/Nevanlinna/laplace2.lean
+++ b/Nevanlinna/laplace2.lean
@@ -12,13 +12,35 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDim
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
 
 
+lemma vectorPresentation'
+  [Fintype ι]
+  (b : OrthonormalBasis ι ℝ E)
+  --(hb : Orthonormal ℝ b)
+  (v : E) :
+  v = ∑ i, ⟪b i, v⟫_ℝ • (b i) := by
+
+  let A :=  b.sum_repr v
+  let i : ι := by sorry
+  let B := b.repr v i
+
+
+  nth_rw 1 [← (b.sum_repr v)]
+  apply Fintype.sum_congr
+  intro i
+  --let A := b.repr v
+  --have : (b.repr v) = ((OrthonormalBasis.toBasis b).repr v) := by tauto
+  rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
+  simp
+
+
+
 lemma vectorPresentation
   [Fintype ι]
   (b : Basis ι ℝ E)
   (hb : Orthonormal ℝ b)
   (v : E) :
   v = ∑ i, ⟪b i, v⟫_ℝ • (b i) := by
-  nth_rw 1 [← (b.sum_repr v)] 
+  nth_rw 1 [← (b.sum_repr v)]
   apply Fintype.sum_congr
   intro i
   rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
@@ -31,7 +53,7 @@ theorem BilinearCalc
   (c : ι → ℝ)
   (L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) :
   L (fun _ => ∑ j : ι, c j • v j) = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L ((fun i => v (x i))) := by
-  
+
   rw [L.map_sum]
   conv =>
     left
@@ -67,7 +89,7 @@ lemma fin_sum
   rw [← Fintype.sum_prod_type']
   apply Fintype.sum_equiv (finTwoArrowEquiv ι)
   intro x
-  dsimp 
+  dsimp
 
 
 theorem LaplaceIndep
@@ -80,9 +102,9 @@ theorem LaplaceIndep
   ∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => v₂ i) := by
 
   have vector_vs_function
-    {y : Fin 2 → ι} 
+    {y : Fin 2 → ι}
     {v : ι → E}
-    : (fun i => v (y i)) = ![v (y 0), v (y 1)] := by 
+    : (fun i => v (y i)) = ![v (y 0), v (y 1)] := by
     funext i
     by_cases h : i = 0
     · rw [h]
@@ -107,13 +129,13 @@ theorem LaplaceIndep
   simp
 
   rw [fin_sum (fun i₀ ↦ (fun i₁ ↦ ⟪v₁ i₀, v₁ i₁⟫_ℝ • L ![v₁ i₀, v₁ i₁]))]
-    
+
   have xx {r₀ : ι} : ∀ r₁ : ι, r₁ ≠ r₀ → ⟪v₁ r₀, v₁ r₁⟫_ℝ • L ![v₁ r₀, v₁ r₁] = 0 := by
     intro r₁ hr₁
     rw [orthonormal_iff_ite.1 hv₁]
     simp
     tauto
-    
+
   conv =>
     right
     arg 2
@@ -142,7 +164,7 @@ theorem LaplaceIndep'
   (hv₁ : Orthonormal ℝ v₁)
   (v₂ : Basis ι ℝ E)
   (hv₂ : Orthonormal ℝ v₂)
-  (f : E → F) 
+  (f : E → F)
   : (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
 
   funext z
@@ -150,7 +172,7 @@ theorem LaplaceIndep'
   let XX := LaplaceIndep v₁ hv₁ v₂ hv₂ (iteratedFDeriv ℝ 2 f z)
   have vector_vs_function
     {v : E}
-    : ![v, v] = (fun _ => v) := by 
+    : ![v, v] = (fun _ => v) := by
     funext i
     by_cases h : i = 0
     · rw [h]
@@ -177,7 +199,7 @@ theorem LaplaceIndep''
   [Fintype ι₂] [DecidableEq ι₂]
   (v₂ : Basis ι₂ ℝ E)
   (hv₂ : Orthonormal ℝ v₂)
-  (f : E → F) 
+  (f : E → F)
   : (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
 
   have b : ι₁ ≃ ι₂ := by
@@ -186,9 +208,9 @@ theorem LaplaceIndep''
     rw [← FiniteDimensional.finrank_eq_card_basis v₂]
 
   let v'₁ := Basis.reindex v₁ b
-  have hv'₁ : Orthonormal ℝ v'₁ := by 
+  have hv'₁ : Orthonormal ℝ v'₁ := by
     let A := Basis.reindex_apply v₁ b
-    have : ⇑v'₁ = v₁ ∘ b.symm := by 
+    have : ⇑v'₁ = v₁ ∘ b.symm := by
       funext i
       exact A i
     rw [this]
@@ -209,7 +231,7 @@ theorem LaplaceIndep''
 
 
 noncomputable def Laplace
-  (f : E → F) 
+  (f : E → F)
   : E → F := by
   exact Laplace_wrt_basis (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal f
 
@@ -218,11 +240,11 @@ theorem LaplaceIndep'''
   [Fintype ι] [DecidableEq ι]
   (v : Basis ι ℝ E)
   (hv : Orthonormal ℝ v)
-  (f : E → F) 
+  (f : E → F)
   : (Laplace f) = (Laplace_wrt_basis v hv f) := by
 
   unfold Laplace
-  apply LaplaceIndep'' (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal v hv f 
+  apply LaplaceIndep'' (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal v hv f
 
 
 theorem Complex.Laplace'
@@ -232,4 +254,3 @@ theorem Complex.Laplace'
   rw [LaplaceIndep''' Complex.orthonormalBasisOneI.toBasis Complex.orthonormalBasisOneI.orthonormal f]
   unfold Laplace_wrt_basis
   simp
-