Update laplace2.lean

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,63 +11,225 @@ 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
+
+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)] 
+  apply Fintype.sum_congr
+  intro i
+  rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
+  simp
 
 
-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₂
+theorem BilinearCalc
   [Fintype ι]
   (v : Basis ι ℝ E)
-  (hv : Orthonormal ℝ v)
-  (f : E → F) :
-  E → F :=
-  fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
+  (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
+    arg 2
+    intro r
+    rw [L.map_smul_univ]
+  simp
+
+
+lemma c2
+  [Fintype ι]
+  (b : Basis ι ℝ E)
+  (hb : Orthonormal ℝ b)
+  (x y : E) :
+  ⟪x, y⟫_ℝ = ∑ i : ι, ⟪x, b i⟫_ℝ * ⟪y, b i⟫_ℝ := by
+  rw [vectorPresentation b hb x]
+  rw [vectorPresentation b hb y]
+  rw [Orthonormal.inner_sum hb]
+  simp
+  conv =>
+    right
+    arg 2
+    intro i'
+    rw [Orthonormal.inner_left_fintype hb]
+    rw [Orthonormal.inner_left_fintype hb]
+
+
+lemma fin_sum
+  [Fintype ι]
+  (f : ι → ι → F) :
+  ∑ r : Fin 2 → ι, f (r 0) (r 1) = ∑ r₀ : ι, (∑ r₁ : ι, f r₀ r₁) := by
+
+  rw [← Fintype.sum_prod_type']
+  apply Fintype.sum_equiv (finTwoArrowEquiv ι)
+  intro x
+  dsimp 
 
-#check ContinuousMultilinearMap.map_sum_finset
 
 theorem LaplaceIndep
-  [Fintype ι]
+  [Fintype ι] [DecidableEq ι]
   (v₁ : Basis ι ℝ E)
   (hv₁ : Orthonormal ℝ v₁)
   (v₂ : Basis ι ℝ E)
   (hv₂ : Orthonormal ℝ v₂)
+  (L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↦ E) F) :
+  ∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => v₂ i) := by
+
+  have vector_vs_function
+    {y : Fin 2 → ι} 
+    {v : ι → E}
+    : (fun i => v (y i)) = ![v (y 0), v (y 1)] := by 
+    funext i
+    by_cases h : i = 0
+    · rw [h]
+      simp
+    · rw [Fin.eq_one_of_neq_zero i h]
+      simp
+
+  conv =>
+    right
+    arg 2
+    intro i
+    rw [vectorPresentation v₁ hv₁ (v₂ i)]
+    rw [BilinearCalc]
+  rw [Finset.sum_comm]
+  conv =>
+    right
+    arg 2
+    intro y
+    rw [← Finset.sum_smul]
+    rw [← c2 v₂ hv₂ (v₁ (y 0)) (v₁ (y 1))]
+    rw [vector_vs_function]
+  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
+    intro r₀
+    rw [Fintype.sum_eq_single r₀ xx]
+    rw [orthonormal_iff_ite.1 hv₁]
+  apply sum_congr
+  rfl
+  intro x _
+  rw [vector_vs_function]
+  simp
+
+
+noncomputable def Laplace_wrt_basis
+  [Fintype ι]
+  (v : Basis ι ℝ E)
+  (_ : Orthonormal ℝ v)
   (f : E → F) :
-  ∑ i, iteratedFDeriv ℝ 2 f z ![v₁ i, v₁ i] =   ∑ i, iteratedFDeriv ℝ 2 f z ![v₂ i, v₂ i] := by
+  E → F :=
+  fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]
 
-  have (v : E) : v = ∑ j, ⟪v₁ j, v⟫_ℝ • (v₁ j) :=
-    sorry
 
+theorem LaplaceIndep'
+  [Fintype ι] [DecidableEq ι]
+  (v₁ : Basis ι ℝ E)
+  (hv₁ : Orthonormal ℝ v₁)
+  (v₂ : Basis ι ℝ E)
+  (hv₂ : Orthonormal ℝ v₂)
+  (f : E → F) 
+  : (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
+
+  funext z
+  unfold Laplace_wrt_basis
+  let XX := LaplaceIndep v₁ hv₁ v₂ hv₂ (iteratedFDeriv ℝ 2 f z)
+  have vector_vs_function
+    {v : E}
+    : ![v, v] = (fun _ => v) := by 
+    funext i
+    by_cases h : i = 0
+    · rw [h]
+      simp
+    · rw [Fin.eq_one_of_neq_zero i h]
+      simp
+  conv =>
+    left
+    arg 2
+    intro i
+    rw [vector_vs_function]
   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]
+    rw [vector_vs_function]
+  assumption
 
-  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
-    (iteratedFDeriv ℝ 2 f z)
-    (fun _ ↦ (fun j ↦ ⟪v₁ j, v⟫_ℝ • (v₁ j)))
+theorem LaplaceIndep''
+  [Fintype ι₁] [DecidableEq ι₁]
+  (v₁ : Basis ι₁ ℝ E)
+  (hv₁ : Orthonormal ℝ v₁)
+  [Fintype ι₂] [DecidableEq ι₂]
+  (v₂ : Basis ι₂ ℝ E)
+  (hv₂ : Orthonormal ℝ v₂)
+  (f : E → F) 
+  : (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
+
+  have b : ι₁ ≃ ι₂ := by
+    apply Fintype.equivOfCardEq
+    rw [← FiniteDimensional.finrank_eq_card_basis v₁]
+    rw [← FiniteDimensional.finrank_eq_card_basis v₂]
+
+  let v'₁ := Basis.reindex v₁ b
+  have hv'₁ : Orthonormal ℝ v'₁ := by 
+    let A := Basis.reindex_apply v₁ b
+    have : ⇑v'₁ = v₁ ∘ b.symm := by 
+      funext i
+      exact A i
+    rw [this]
+    let B := Orthonormal.comp hv₁ b.symm
+    apply B
+    exact Equiv.injective b.symm
+  rw [← LaplaceIndep' v'₁ hv'₁ v₂ hv₂ f]
+
+  unfold Laplace_wrt_basis
+  simp
+  funext z
+
+  rw [← Equiv.sum_comp b.symm]
+  apply Fintype.sum_congr
+  intro i₂
+  congr
+  rw [Basis.reindex_apply v₁ b i₂]
+
+
+noncomputable def Laplace
+  (f : E → F) 
+  : E → F := by
+  exact Laplace_wrt_basis (stdOrthonormalBasis ℝ E).toBasis (stdOrthonormalBasis ℝ E).orthonormal f
+
+
+theorem LaplaceIndep'''
+  [Fintype ι] [DecidableEq ι]
+  (v : Basis ι ℝ E)
+  (hv : Orthonormal ℝ v)
+  (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 
+
+
+theorem Complex.Laplace'
+  (f : ℂ → F)
+  : (Laplace f) = fun z ↦ (iteratedFDeriv ℝ 2 f z) ![1, 1] + (iteratedFDeriv ℝ 2 f z) ![Complex.I, Complex.I] := by
+
+  rw [LaplaceIndep''' Complex.orthonormalBasisOneI.toBasis Complex.orthonormalBasisOneI.orthonormal f]
+  unfold Laplace_wrt_basis
+  simp
 
-  --
-  --  (fun _ ↦ Finset.univ)
-  simp at X
-  
-  sorry