nevanlinna/Nevanlinna/laplace2.lean

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
import Mathlib.LinearAlgebra.Basis

open BigOperators
open Finset

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]


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


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]

  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)))

  --
  --  (fun _ ↦ Finset.univ)
  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]