@@ -1,172 +1,89 @@
--import Mathlib.Algebra.BigOperators.Basic
import Mathlib . Analysis . InnerProductSpace . Basic
import Mathlib . Analysis . InnerProductSpace . Dual
/-
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
/- !
open BigOperators
open Finset
# Canoncial Elements in Tensor Powers of Real Inner Product Spaces
variable { E : Type * } [ NormedAddCommGroup E ] [ InnerProductSpace ℝ E ] [ FiniteDimensional ℝ E ]
variable { F : Type * } [ NormedAddCommGroup F ] [ NormedSpace ℝ F ]
open BigOperators
open Finset
Given an `InnerProductSpace ℝ
are relevant when for a coordinate - free definition of differential operators
such as the Laplacian.
* `InnerProductSpace.canonicalContravariantTensor E : E ⊗[ℝ ℝ ℝ
the element corresponding to the inner product.
* If `E` is finite - dimensional, then `E ⊗[ℝ
dual. Accordingly, there exists an element
`InnerProductSpace.canonicalCovariantTensor E : E ⊗[ℝ
`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) ⊗ₜ[ℝ
-/
open TensorProduct
lemma vectorPresentation
lemma OrthonormalBasis . sum_repr'
{ 𝕜 : Type * } [ RCLike 𝕜 ]
{ E : Type * } [ NormedAddCommGroup E ] [ InnerProductSpace 𝕜 E ]
[ Fintype ι ]
( b : Basis ι ℝ E )
( hb : Orthonormal ℝ b )
( b : Orthonormal Basis ι 𝕜 E )
( 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 ) ]
apply Fintype . sum_congr
intro i
rw [ ← Orthonormal . inner_right_finsupp hb ( b . repr v ) i ]
simp
simp_rw [ b . repr_apply_apply v ]
theorem BilinearCalc
noncomputable def InnerProductSpace . canonicalContravariantTensor
{ 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 : 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
( v : Orthonormal Basis ι ℝ E )
: InnerProductSpace . canonicalCovariantTensor E = ∑ i , ( v i ) ⊗ ₜ [ ℝ ] ( v i ) : = by
let w : = stdOrthonormalBasis ℝ E
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
rw [ w . sum_repr' ( v i ) ]
simp_ rw [ TensorProduct . sum_tmul , TensorProduct . tmul_sum , TensorProduct . smul_tmul_smul
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
rw [ Finset . sum_comm ]
arg 2
intro r₀
rw [ Fintype . sum_eq_single r₀ xx ]
rw [ orthonormal_iff_ite . 1 hv₁ ]
apply sum_congr
intro x
rw [ ← Finset . sum_smul ]
arg 1
arg 2
intro i
rw [ ← real_inner_comm ( w x ) ]
simp_rw [ OrthonormalBasis . sum_inner_mul_inner v ]
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
intro x _
rw [ vector_vs_function ]
simp
