Compare commits

..

3 Commits

Author SHA1 Message Date
Stefan Kebekus 323b133c88 working... 2024-06-29 17:17:19 +02:00
Stefan Kebekus 602296031d Update bilinear.lean 2024-06-29 09:17:43 +02:00
Stefan Kebekus 8b4317759c Update bilinear.lean 2024-06-29 09:01:53 +02:00
2 changed files with 107 additions and 153 deletions

View File

@ -1,172 +1,89 @@
--import Mathlib.Algebra.BigOperators.Basic /-
import Mathlib.Analysis.InnerProductSpace.Basic Copyright (c) 2024 Stefan Kebekus. All rights reserved.
import Mathlib.Analysis.InnerProductSpace.Dual Released under Apache 2.0 license as described in the file LICENSE.
Authors: Stefan Kebekus
-/
import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.InnerProductSpace.PiL2
/-!
open BigOperators # Canoncial Elements in Tensor Powers of Real Inner Product Spaces
open Finset
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E] Given an `InnerProductSpace E`, this file defines two canonical tensors, which
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F] are relevant when for a coordinate-free definition of differential operators
open BigOperators such as the Laplacian.
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 ι] [Fintype ι]
(b : Basis ι E) (b : OrthonormalBasis ι 𝕜 E)
(hb : Orthonormal b)
(v : 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)] nth_rw 1 [← (b.sum_repr v)]
apply Fintype.sum_congr simp_rw [b.repr_apply_apply v]
intro i
rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i]
simp
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 ι] [Fintype ι]
(v : Basis ι E) (v : OrthonormalBasis ι E)
(c : ι) : InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[] (v i) := by
(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
let w := stdOrthonormalBasis E
conv => conv =>
right right
arg 2 arg 2
intro i intro i
rw [vectorPresentation v₁ hv₁ (v₂ i)] rw [w.sum_repr' (v i)]
rw [TensorProduct.sum_tmul] simp_rw [TensorProduct.sum_tmul, TensorProduct.tmul_sum, TensorProduct.smul_tmul_smul]
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 => conv =>
right right
arg 2
intro i
rw [vectorPresentation v₁ hv₁ (v₂ i)]
rw [BilinearCalc]
rw [Finset.sum_comm] rw [Finset.sum_comm]
conv =>
right
arg 2 arg 2
intro y intro y
rw [← Finset.sum_smul] rw [Finset.sum_comm]
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 arg 2
intro r₀ intro x
rw [Fintype.sum_eq_single r₀ xx] rw [← Finset.sum_smul]
rw [orthonormal_iff_ite.1 hv₁] arg 1
apply sum_congr 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 rfl
intro x _
rw [vector_vs_function]
simp

View File

@ -10,7 +10,6 @@ import Mathlib.LinearAlgebra.Contraction
open BigOperators open BigOperators
open Finset open Finset
lemma OrthonormalBasis.sum_repr' lemma OrthonormalBasis.sum_repr'
{𝕜 : Type*} [RCLike 𝕜] {𝕜 : Type*} [RCLike 𝕜]
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
@ -21,15 +20,53 @@ lemma OrthonormalBasis.sum_repr'
nth_rw 1 [← (b.sum_repr v)] nth_rw 1 [← (b.sum_repr v)]
simp_rw [b.repr_apply_apply v] simp_rw [b.repr_apply_apply v]
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E]
noncomputable def realInnerAsElementOfDualTensorprod noncomputable def realInnerAsElementOfDualTensorprod
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] {E : Type*} [NormedAddCommGroup E] [InnerProductSpace E]
: TensorProduct E E →ₗ[] := TensorProduct.lift bilinFormOfRealInner : 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' noncomputable def dual'
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [CompleteSpace E] [FiniteDimensional E] {E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [CompleteSpace E] [FiniteDimensional E]
: (TensorProduct E E →ₗ[] ) ≃ₗ[] TensorProduct E E := by : (TensorProduct E E →ₗ[] ) ≃ₗ[] TensorProduct E E := by
let d := InnerProductSpace.toDual E let d := InnerProductSpace.toDual E
let e := d.toLinearEquiv let e := d.toLinearEquiv
let a := TensorProduct.congr e e let a := TensorProduct.congr e e