import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
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
import Mathlib.LinearAlgebra.Contraction

open BigOperators
open Finset


lemma OrthonormalBasis.sum_repr'
  {𝕜 : Type*} [RCLike 𝕜]
  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [Fintype ι]
  (b : OrthonormalBasis ι 𝕜 E)
  (v : E) :
  v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
  nth_rw 1 [← (b.sum_repr v)]
  simp_rw [b.repr_apply_apply v]

noncomputable def realInnerAsElementOfDualTensorprod
  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  : TensorProduct ℝ E E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner

noncomputable def dual'
  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]  [FiniteDimensional ℝ E]
  : (TensorProduct ℝ E E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] TensorProduct ℝ E E := by

  let d := InnerProductSpace.toDual ℝ E
  let e := d.toLinearEquiv

  let a := TensorProduct.congr e e

  let b := homTensorHomEquiv ℝ E E ℝ ℝ

  sorry


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


theorem InvariantTensor
  [Fintype ι]
  (v : Basis ι ℝ E)
  (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]
  simp_rw [L.map_smul_univ]
  sorry



theorem BilinearCalc
  [Fintype ι]
  (v : Basis ι ℝ E)
  (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]
  simp_rw [L.map_smul_univ]
  sorry

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


theorem LaplaceIndep
  [Fintype ι] [DecidableEq ι]
  (v₁ : OrthonormalBasis ι ℝ E)
  (v₂ : OrthonormalBasis ι ℝ E)
  (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 [v₁.sum_repr' (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) :
  E → F :=
  fun z ↦ ∑ i, iteratedFDeriv ℝ 2 f z ![v i, v i]


theorem LaplaceIndep'
  [Fintype ι] [DecidableEq ι]
  (v₁ : OrthonormalBasis ι ℝ E)
  (v₂ : OrthonormalBasis ι ℝ E)
  (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 [vector_vs_function]
  assumption


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