From 323b133c88ff48d4a01ae5a9b3ecfa9738ddcd91 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Sat, 29 Jun 2024 17:17:19 +0200
Subject: [PATCH] working...

---
 Nevanlinna/bilinear.lean | 65 +++++++++++++++++++++++++++++-----------
 Nevanlinna/laplace2.lean | 39 +++++++++++++++++++++++-
 2 files changed, 86 insertions(+), 18 deletions(-)

diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean
index ea1d5a1..1ed7b86 100644
--- a/Nevanlinna/bilinear.lean
+++ b/Nevanlinna/bilinear.lean
@@ -1,5 +1,34 @@
+/-
+Copyright (c) 2024 Stefan Kebekus. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Stefan Kebekus
+-/
+
 import Mathlib.Analysis.InnerProductSpace.PiL2
 
+/-!
+
+# Canoncial Elements in Tensor Powers of Real Inner Product Spaces
+
+Given an `InnerProductSpace ℝ E`, this file defines two canonical tensors, which
+are relevant when for a coordinate-free definition of differential operators
+such as the Laplacian.
+
+* `InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ] E →ₗ[ℝ] ℝ`. This is
+  the element corresponding to the inner product.
+
+* If `E` is finite-dimensional, then `E ⊗[ℝ] E` is canonically isomorphic to its
+  dual. Accordingly, there exists an element
+  `InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ] E` that corresponds to
+  `InnerProductSpace.canonicalContravariantTensor E` under this identification.
+
+The theorem `InnerProductSpace.canonicalCovariantTensorRepresentation` shows
+that `InnerProductSpace.canonicalCovariantTensor E` can be computed from any
+orthonormal basis `v` as `∑ i, (v i) ⊗ₜ[ℝ] (v i)`.
+
+-/
+
+
 open TensorProduct
 
 
@@ -14,26 +43,28 @@ lemma OrthonormalBasis.sum_repr'
   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)
+noncomputable def InnerProductSpace.canonicalContravariantTensor
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
+  : E ⊗[ℝ] E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner
 
 
-theorem InnerProductSpace.InvariantTensor
+noncomputable def InnerProductSpace.canonicalCovariantTensor
+  (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] 
+  : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i)
+
+
+theorem InnerProductSpace.canonicalCovariantTensorRepresentation
   (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
+  [Fintype ι]
+  (v : OrthonormalBasis ι ℝ E)
+  : InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
 
+  let w := stdOrthonormalBasis ℝ E
   conv =>
     right
     arg 2
     intro i
-    rw [v₁.sum_repr' (v i)]
+    rw [w.sum_repr' (v i)]
   simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
   
   conv =>
@@ -48,11 +79,11 @@ theorem InnerProductSpace.InvariantTensor
     arg 1
     arg 2
     intro i
-    rw [← real_inner_comm (v₁ x)]
+    rw [← real_inner_comm (w x)]
   simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
 
-  have {x : Fin (FiniteDimensional.finrank ℝ E)} : ∑ x_1 : Fin (FiniteDimensional.finrank ℝ E), ⟪v₁ x, v₁ x_1⟫_ℝ • v₁ x ⊗ₜ[ℝ] v₁ x_1 = v₁ x ⊗ₜ[ℝ] v₁ x := by
-    rw [Fintype.sum_eq_single x, orthonormal_iff_ite.1 v₁.orthonormal]; simp
-    intro r₁ hr₁
-    rw [orthonormal_iff_ite.1 v₁.orthonormal]; simp; tauto
+  have {i} : ∑ j, ⟪w i, w j⟫_ℝ • w i ⊗ₜ[ℝ] w j = w i ⊗ₜ[ℝ] w i := by
+    rw [Fintype.sum_eq_single i, orthonormal_iff_ite.1 w.orthonormal]; simp
+    intro _ _; rw [orthonormal_iff_ite.1 w.orthonormal]; simp; tauto
   simp_rw [this]
+  rfl
diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean
index cdc5023..cf95e5a 100644
--- a/Nevanlinna/laplace2.lean
+++ b/Nevanlinna/laplace2.lean
@@ -10,7 +10,6 @@ import Mathlib.LinearAlgebra.Contraction
 open BigOperators
 open Finset
 
-
 lemma OrthonormalBasis.sum_repr'
   {𝕜 : Type*} [RCLike 𝕜]
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
@@ -21,15 +20,53 @@ lemma OrthonormalBasis.sum_repr'
   nth_rw 1 [← (b.sum_repr v)]
   simp_rw [b.repr_apply_apply v]
 
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
+
 noncomputable def realInnerAsElementOfDualTensorprod
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
   : TensorProduct ℝ E E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner
 
+
+instance 
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]  [FiniteDimensional ℝ E]
+  : NormedAddCommGroup (TensorProduct ℝ E E) where 
+    norm := by 
+      
+      sorry
+    dist_self := by 
+      
+      sorry
+
+  sorry
+
+/-
+instance 
+  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]  [FiniteDimensional ℝ E]
+  : InnerProductSpace ℝ (TensorProduct ℝ E E) where
+    smul := _
+    one_smul := _
+    mul_smul := _
+    smul_zero := _
+    smul_add := _
+    add_smul := _
+    zero_smul := _
+    norm_smul_le := _
+    inner := _
+    norm_sq_eq_inner := _
+    conj_symm := _
+    add_left := _
+    smul_left := _
+  -/
+
+
+
 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