Nevanlinna/bilinear.lean

@@ -1,89 +1,172 @@
-/-
+--import Mathlib.Algebra.BigOperators.Basic
-Copyright (c) 2024 Stefan Kebekus. All rights reserved.
+import Mathlib.Analysis.InnerProductSpace.Basic
-Released under Apache 2.0 license as described in the file LICENSE.
+import Mathlib.Analysis.InnerProductSpace.Dual
-Authors: Stefan Kebekus
--/
-
 import Mathlib.Analysis.InnerProductSpace.PiL2
 
-/-!
 
-# Canoncial Elements in Tensor Powers of Real Inner Product Spaces
+open BigOperators
+open Finset
 
-Given an `InnerProductSpace ℝ E`, this file defines two canonical tensors, which
+variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
-are relevant when for a coordinate-free definition of differential operators
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
-such as the Laplacian.
+open BigOperators
-
+open Finset
-* `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
 
-
+lemma vectorPresentation
-lemma OrthonormalBasis.sum_repr'
-  {𝕜 : Type*} [RCLike 𝕜]
-  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
   [Fintype ι]
-  (b : OrthonormalBasis ι 𝕜 E)
+  (b : Basis ι ℝ E)
+  (hb : Orthonormal ℝ b)
   (v : E) :
-  v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
+  v = ∑ i, ⟪b i, v⟫_ℝ • (b i) := by
-  nth_rw 1 [← (b.sum_repr v)]
+  nth_rw 1 [← (b.sum_repr v)] 
-  simp_rw [b.repr_apply_apply v]
+  apply Fintype.sum_congr
+  intro i
+  rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
+  simp
 
 
-noncomputable def InnerProductSpace.canonicalContravariantTensor
+theorem BilinearCalc
-  {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
-  : E ⊗[ℝ] E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner
-
-
-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]
   [Fintype ι]
-  (v : OrthonormalBasis ι ℝ E)
+  (v : Basis ι ℝ E)
-  : InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
+  (c : ι → ℝ)
-
+  (L : E →ₗ[ℝ] E →ₗ[ℝ] F) 
-  let w := stdOrthonormalBasis ℝ E
+  : L (∑ j : ι, c j • v j) (∑ j : ι, c j • v j) 
-  conv =>
+    = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L (v (x 0)) (v (x 1)) := by
-    right
-    arg 2
-    intro i
-    rw [w.sum_repr' (v i)]
-  simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
   
+  rw [map_sum]
+  rw [map_sum]
+
   conv =>
-    right
+    left
-    rw [Finset.sum_comm]
     arg 2
-    intro y
+    intro r
-    rw [Finset.sum_comm]
+    rw [← sum_apply]
+
+    rw [map_smul]
     arg 2
-    intro x
-    rw [← Finset.sum_smul]
     arg 1
     arg 2
-    intro i
+    intro x
-    rw [← real_inner_comm (w x)]
+    rw [map_smul]
-  simp_rw [OrthonormalBasis.sum_inner_mul_inner v]
+  simp
 
-  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
+lemma c2
-    intro _ _; rw [orthonormal_iff_ite.1 w.orthonormal]; simp; tauto
+  [Fintype ι]
-  simp_rw [this]
+  (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

Nevanlinna/laplace2.lean

@@ -10,6 +10,7 @@ import Mathlib.LinearAlgebra.Contraction
 open BigOperators
 open Finset
 
+
 lemma OrthonormalBasis.sum_repr'
   {𝕜 : Type*} [RCLike 𝕜]
   {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
@@ -20,53 +21,15 @@ 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