From 8b4317759c7af4bcea7baca27a81aecf76fb64b4 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sat, 29 Jun 2024 09:01:53 +0200
Subject: [PATCH] Update bilinear.lean

---
 Nevanlinna/bilinear.lean | 187 +++++++++------------------------------
 1 file changed, 44 insertions(+), 143 deletions(-)

diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean
index 54869fc..02c514a 100644
--- a/Nevanlinna/bilinear.lean
+++ b/Nevanlinna/bilinear.lean
@@ -1,172 +1,73 @@
 --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]
-open BigOperators
-open Finset
 
 
 
-lemma vectorPresentation
+lemma OrthonormalBasis.sum_repr'
+  {𝕜 : Type*} [RCLike 𝕜]
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
   [Fintype ι]
-  (b : Basis ι ℝ E)
-  (hb : Orthonormal ℝ b)
+  (b : OrthonormalBasis ι 𝕜 E)
   (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]
+  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
 
-
-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
+  conv =>
+    right
+    arg 2
+    intro i
+    rw [v₁.sum_repr' (v₂ i)]
+  simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
   
-  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_comm]
+    arg 2
+    intro x
     rw [← Finset.sum_smul]
-    rw [← c2 v₂ hv₂ (v₁ (y 0)) (v₁ (y 1))]
-    rw [vector_vs_function]
-  simp
+    arg 1
+    arg 2
+    intro i
+    rw [← real_inner_comm (v₁ x)]
+  simp_rw [OrthonormalBasis.sum_inner_mul_inner v₂]
 
-  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
+  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 hv₁]
+    rw [orthonormal_iff_ite.1 v₁.orthonormal]
     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_rw [Fintype.sum_eq_single _ xx]
+  simp_rw [orthonormal_iff_ite.1 v₁.orthonormal]
   simp