Compare commits
No commits in common. "323b133c88ff48d4a01ae5a9b3ecfa9738ddcd91" and "9a9fbf1b549a636283d57aafffb0b2d552544d5f" have entirely different histories.
323b133c88
...
9a9fbf1b54
|
|
@ -1,89 +1,172 @@
|
|||
/-
|
||||
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.Algebra.BigOperators.Basic
|
||||
import Mathlib.Analysis.InnerProductSpace.Basic
|
||||
import Mathlib.Analysis.InnerProductSpace.Dual
|
||||
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
|
||||
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)`.
|
||||
|
||||
-/
|
||||
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
|
||||
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
|
||||
open BigOperators
|
||||
open Finset
|
||||
|
||||
|
||||
open TensorProduct
|
||||
|
||||
|
||||
lemma OrthonormalBasis.sum_repr'
|
||||
{𝕜 : Type*} [RCLike 𝕜]
|
||||
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
|
||||
lemma vectorPresentation
|
||||
[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)]
|
||||
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
|
||||
{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]
|
||||
theorem BilinearCalc
|
||||
[Fintype ι]
|
||||
(v : OrthonormalBasis ι ℝ E)
|
||||
: InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[ℝ] (v i) := by
|
||||
(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
|
||||
|
||||
let w := stdOrthonormalBasis ℝ E
|
||||
conv =>
|
||||
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
|
||||
rw [Finset.sum_comm]
|
||||
left
|
||||
arg 2
|
||||
intro y
|
||||
rw [Finset.sum_comm]
|
||||
intro r
|
||||
rw [← sum_apply]
|
||||
|
||||
rw [map_smul]
|
||||
arg 2
|
||||
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]
|
||||
intro x
|
||||
rw [map_smul]
|
||||
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
|
||||
intro _ _; rw [orthonormal_iff_ite.1 w.orthonormal]; simp; tauto
|
||||
simp_rw [this]
|
||||
|
||||
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_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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Reference in New Issue