--import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.PiL2


open BigOperators
open Finset

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



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 BilinearCalc
  [Fintype ι]
  (v : Basis ι ℝ E)
  (c : ι → ℝ)
  (L : E →ₗ[ℝ] E →ₗ[ℝ] F) 
  : L (∑ j : ι, c j • v j) (∑ j : ι, c j • v j) 
    = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L (v (x 0)) (v (x 1)) := by
  
  rw [map_sum]
  rw [map_sum]

  conv =>
    left
    arg 2
    intro r
    rw [← sum_apply]

    rw [map_smul]
    arg 2
    arg 1
    arg 2
    intro x
    rw [map_smul]
  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 

theorem TensorIndep
  [Fintype ι] [DecidableEq ι]
  (v₁ : Basis ι ℝ E)
  (hv₁ : Orthonormal ℝ v₁)
  (v₂ : Basis ι ℝ E)
  (hv₂ : Orthonormal ℝ v₂) :
  ∑ i, (v₁ i) ⊗ₜ[ℝ] (v₁ i) = ∑ i, (v₂ i) ⊗ₜ[ℝ] (v₂ i) := by

  conv =>
    right
    arg 2
    intro i
    rw [vectorPresentation v₁ hv₁ (v₂ i)]
    rw [TensorProduct.sum_tmul]
    arg 2
    intro j
    rw [TensorProduct.tmul_sum]
    arg 2
    intro a
    rw [TensorProduct.tmul_smul]
    arg 2
    rw [TensorProduct.smul_tmul]

  rw [Finset.sum_comm]
  conv =>
    right
    arg 2
    intro i
    rw [Finset.sum_comm]



  sorry

theorem LaplaceIndep
  [Fintype ι] [DecidableEq ι]
  (v₁ : Basis ι ℝ E)
  (hv₁ : Orthonormal ℝ v₁)
  (v₂ : Basis ι ℝ E)
  (hv₂ : Orthonormal ℝ v₂)
  (L : E →ₗ[ℝ] E →ₗ[ℝ] F) :
  ∑ i, L (v₁ i) (v₁ i) = ∑ i, L (v₂ i) (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