nevanlinna/Nevanlinna/bilinear.lean

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

open BigOperators
open Finset
open scoped TensorProduct

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



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 InnerProductSpace.canonicalTensor
  (E : Type u_2) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] 
  : E ⊗[ℝ] E := by
  let v := stdOrthonormalBasis ℝ E
  exact ∑ i, (v i) ⊗ₜ[ℝ] (v i)


theorem InnerProductSpace.InvariantTensor
  (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  (v₂ : OrthonormalBasis (Fin (FiniteDimensional.finrank ℝ E)) ℝ E)
  : InnerProductSpace.canonicalTensor E = ∑ i, (v₂ i) ⊗ₜ[ℝ] (v₂ i) := by

  unfold InnerProductSpace.canonicalTensor

  let v₁ := stdOrthonormalBasis ℝ E
  simp

  conv =>
    right
    arg 2
    intro i
    rw [v₁.sum_repr' (v₂ i)]
  simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
  
  conv =>
    right
    rw [Finset.sum_comm]
    arg 2
    intro y
    rw [Finset.sum_comm]
    arg 2
    intro x
    rw [← Finset.sum_smul]
    arg 1
    arg 2
    intro i
    rw [← real_inner_comm (v₁ x)]
  simp_rw [OrthonormalBasis.sum_inner_mul_inner v₂]

  have xx {r₀ : Fin (FiniteDimensional.finrank ℝ E)} : ∀ r₁ : Fin (FiniteDimensional.finrank ℝ E), r₁ ≠ r₀ → ⟪v₁ r₀, v₁ r₁⟫_ℝ • v₁ r₀ ⊗ₜ[ℝ] v₁ r₁ = 0 := by
    intro r₁ hr₁
    rw [orthonormal_iff_ite.1 v₁.orthonormal]
    simp
    tauto
  simp_rw [Fintype.sum_eq_single _ xx]
  simp_rw [orthonormal_iff_ite.1 v₁.orthonormal]
  simp