Compare commits

...

14 Commits

Author SHA1 Message Date
Stefan Kebekus ff00a0db82 Update tensor.lean 2024-07-03 11:17:47 +02:00
Stefan Kebekus 36c3d0f66b Create tensor.lean 2024-07-02 11:45:03 +02:00
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
Stefan Kebekus 9a9fbf1b54 Update mathlib 2024-06-28 07:53:20 +02:00
Stefan Kebekus 6412671bc6 Working… 2024-06-27 14:02:00 +02:00
Stefan Kebekus c59e12a468 Update laplace2.lean 2024-06-27 06:35:02 +02:00
Stefan Kebekus 07f4ff610b Create bilinear.lean 2024-06-26 12:28:39 +02:00
Stefan Kebekus c1766f6a38 Update laplace2.lean 2024-06-24 17:30:30 +02:00
Stefan Kebekus 42cf2e41b9 Update laplace2.lean 2024-06-24 12:14:18 +02:00
Stefan Kebekus ecdc182f2b Update laplace2.lean 2024-06-24 08:03:39 +02:00
Stefan Kebekus adc0378e5d Update laplace2.lean 2024-06-24 07:58:04 +02:00
Stefan Kebekus d287c24453 New file 2024-06-23 21:13:01 +02:00
5 changed files with 444 additions and 14 deletions

89
Nevanlinna/bilinear.lean Normal file
View File

@ -0,0 +1,89 @@
/-
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
lemma OrthonormalBasis.sum_repr'
{𝕜 : Type*} [RCLike 𝕜]
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
[Fintype ι]
(b : OrthonormalBasis ι 𝕜 E)
(v : E) :
v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
nth_rw 1 [← (b.sum_repr v)]
simp_rw [b.repr_apply_apply v]
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 : OrthonormalBasis ι E)
: InnerProductSpace.canonicalCovariantTensor E = ∑ i, (v i) ⊗ₜ[] (v i) := 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]
conv =>
right
rw [Finset.sum_comm]
arg 2
intro y
rw [Finset.sum_comm]
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]
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

294
Nevanlinna/laplace2.lean Normal file
View File

@ -0,0 +1,294 @@
import Mathlib.Analysis.InnerProductSpace.Basic
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.PiL2
--import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Analysis.Calculus.ContDiff.Bounds
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.LinearAlgebra.Basis
import Mathlib.LinearAlgebra.Contraction
open BigOperators
open Finset
lemma OrthonormalBasis.sum_repr'
{𝕜 : Type*} [RCLike 𝕜]
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
[Fintype ι]
(b : OrthonormalBasis ι 𝕜 E)
(v : E) :
v = ∑ i, ⟪b i, v⟫_𝕜 • (b i) := by
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
let b := homTensorHomEquiv E E
sorry
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace E] [FiniteDimensional E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace F]
theorem InvariantTensor
[Fintype ι]
(v : Basis ι E)
(c : ι)
(L : ContinuousMultilinearMap (fun (_ : Fin 2) ↦ E) F) :
L (fun _ => ∑ j : ι, c j • v j) = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L ((fun i => v (x i))) := by
rw [L.map_sum]
simp_rw [L.map_smul_univ]
sorry
theorem BilinearCalc
[Fintype ι]
(v : Basis ι E)
(c : ι)
(L : ContinuousMultilinearMap (fun (_ : Fin 2) ↦ E) F) :
L (fun _ => ∑ j : ι, c j • v j) = ∑ x : Fin 2 → ι, (c (x 0) * c (x 1)) • L ((fun i => v (x i))) := by
rw [L.map_sum]
simp_rw [L.map_smul_univ]
sorry
/-
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 LaplaceIndep
[Fintype ι] [DecidableEq ι]
(v₁ : OrthonormalBasis ι E)
(v₂ : OrthonormalBasis ι E)
(L : ContinuousMultilinearMap (fun (_ : Fin 2) ↦ E) F) :
∑ i, L (fun _ ↦ v₁ i) = ∑ i, L (fun _ => 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 [v₁.sum_repr' (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
noncomputable def Laplace_wrt_basis
[Fintype ι]
(v : Basis ι E)
(_ : Orthonormal v)
(f : E → F) :
E → F :=
fun z ↦ ∑ i, iteratedFDeriv 2 f z ![v i, v i]
theorem LaplaceIndep'
[Fintype ι] [DecidableEq ι]
(v₁ : OrthonormalBasis ι E)
(v₂ : OrthonormalBasis ι E)
(f : E → F)
: (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
funext z
unfold Laplace_wrt_basis
let XX := LaplaceIndep v₁ hv₁ v₂ hv₂ (iteratedFDeriv 2 f z)
have vector_vs_function
{v : E}
: ![v, v] = (fun _ => v) := by
funext i
by_cases h : i = 0
· rw [h]
simp
· rw [Fin.eq_one_of_neq_zero i h]
simp
conv =>
left
arg 2
intro i
rw [vector_vs_function]
conv =>
right
arg 2
intro i
rw [vector_vs_function]
assumption
theorem LaplaceIndep''
[Fintype ι₁] [DecidableEq ι₁]
(v₁ : Basis ι₁ E)
(hv₁ : Orthonormal v₁)
[Fintype ι₂] [DecidableEq ι₂]
(v₂ : Basis ι₂ E)
(hv₂ : Orthonormal v₂)
(f : E → F)
: (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by
have b : ι₁ ≃ ι₂ := by
apply Fintype.equivOfCardEq
rw [← FiniteDimensional.finrank_eq_card_basis v₁]
rw [← FiniteDimensional.finrank_eq_card_basis v₂]
let v'₁ := Basis.reindex v₁ b
have hv'₁ : Orthonormal v'₁ := by
let A := Basis.reindex_apply v₁ b
have : ⇑v'₁ = v₁ ∘ b.symm := by
funext i
exact A i
rw [this]
let B := Orthonormal.comp hv₁ b.symm
apply B
exact Equiv.injective b.symm
rw [← LaplaceIndep' v'₁ hv'₁ v₂ hv₂ f]
unfold Laplace_wrt_basis
simp
funext z
rw [← Equiv.sum_comp b.symm]
apply Fintype.sum_congr
intro i₂
congr
rw [Basis.reindex_apply v₁ b i₂]
noncomputable def Laplace
(f : E → F)
: E → F := by
exact Laplace_wrt_basis (stdOrthonormalBasis E).toBasis (stdOrthonormalBasis E).orthonormal f
theorem LaplaceIndep'''
[Fintype ι] [DecidableEq ι]
(v : Basis ι E)
(hv : Orthonormal v)
(f : E → F)
: (Laplace f) = (Laplace_wrt_basis v hv f) := by
unfold Laplace
apply LaplaceIndep'' (stdOrthonormalBasis E).toBasis (stdOrthonormalBasis E).orthonormal v hv f
theorem Complex.Laplace'
(f : → F)
: (Laplace f) = fun z ↦ (iteratedFDeriv 2 f z) ![1, 1] + (iteratedFDeriv 2 f z) ![Complex.I, Complex.I] := by
rw [LaplaceIndep''' Complex.orthonormalBasisOneI.toBasis Complex.orthonormalBasisOneI.orthonormal f]
unfold Laplace_wrt_basis
simp

47
Nevanlinna/tensor.lean Normal file
View File

@ -0,0 +1,47 @@
import Mathlib.Analysis.InnerProductSpace.PiL2
open RCLike Real Filter
open Topology ComplexConjugate
open LinearMap (BilinForm)
open TensorProduct
open InnerProductSpace
open Inner
example
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace E]
{F : Type*} [NormedAddCommGroup F] [InnerProductSpace F]
: 1 = 0 := by
let e : E →ₗ[] E →ₗ[] := innerₗ E
let f : F →ₗ[] F →ₗ[] := innerₗ F
let e₂ := TensorProduct.map₂ e f
let l := TensorProduct.lid
have : ∀ e1 e2 : E, ∀ f1 f2 : F, e₂ (e1 ⊗ f1) (e2 ⊗ f2) =
let X : InnerProductSpace.Core (E ⊗[] F) := {
inner := by
intro a b
exact TensorProduct.lid ((TensorProduct.map₂ (innerₗ E) (innerₗ F)) a b)
conj_symm := by
simp
intro x y
unfold innerₗ
simp
sorry
nonneg_re := _
definite := _
add_left := _
smul_left := _
}
let inner : E ⊗[𝕜] E → E ⊗[𝕜] E → 𝕜 :=
--let x := TensorProduct.lift
--E.inner
--TensorProduct.map₂
sorry
sorry

View File

@ -1,11 +1,11 @@
{"version": 7,
{"version": "1.0.0",
"packagesDir": ".lake/packages",
"packages":
[{"url": "https://github.com/leanprover/std4",
[{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
"name": "std",
"rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
@ -13,7 +13,7 @@
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
"rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
@ -22,25 +22,25 @@
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
"rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inherited": true,
"configFile": "lakefile.lean"},
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
"type": "git",
"subDir": null,
"rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
"rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.30",
"inputRev": "v0.0.38",
"inherited": true,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover/lean4-cli",
"type": "git",
"subDir": null,
"rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
"rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
@ -49,16 +49,16 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
"rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
"inherited": true,
"configFile": "lakefile.lean"},
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/mathlib4.git",
"type": "git",
"subDir": null,
"rev": "e408da18380ef42acf7b8337c6b0536bfac09105",
"rev": "dcc73cfb2ce3763f830c52042fb8617e762dbf60",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": null,

View File

@ -1 +1 @@
leanprover/lean4:v4.7.0
leanprover/lean4:v4.9.0-rc3