From 6412671bc6c08cb84620335336aa23057541d770 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 27 Jun 2024 14:02:00 +0200 Subject: [PATCH] =?UTF-8?q?Working=E2=80=A6?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Nevanlinna/laplace2.lean | 95 ++++++++++++++++++++-------------------- lake-manifest.json | 26 +++++------ lean-toolchain | 2 +- 3 files changed, 62 insertions(+), 61 deletions(-) diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean index dc787ef..7597bac 100644 --- a/Nevanlinna/laplace2.lean +++ b/Nevanlinna/laplace2.lean @@ -1,51 +1,60 @@ 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] + +noncomputable def realInnerAsElementOfDualTensorprod + {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] + : TensorProduct ℝ E E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner + +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] -lemma vectorPresentation' +theorem InvariantTensor [Fintype ι] - (b : OrthonormalBasis ι ℝ E) - --(hb : Orthonormal ℝ b) - (v : E) : - v = ∑ i, ⟪b i, v⟫_ℝ • (b i) := by + (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 - let A := b.sum_repr v - let i : ι := by sorry - let B := b.repr v i + rw [L.map_sum] + simp_rw [L.map_smul_univ] + sorry - nth_rw 1 [← (b.sum_repr v)] - apply Fintype.sum_congr - intro i - --let A := b.repr v - --have : (b.repr v) = ((OrthonormalBasis.toBasis b).repr v) := by tauto - rw [← Orthonormal.inner_right_finsupp hb (b.repr v) i] - simp - - - -lemma vectorPresentation - [Fintype ι] - (b : Basis ι ℝ E) - (hb : Orthonormal ℝ b) - (v : E) : - 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 - theorem BilinearCalc [Fintype ι] @@ -55,14 +64,10 @@ theorem BilinearCalc 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] - conv => - left - arg 2 - intro r - rw [L.map_smul_univ] - simp - + simp_rw [L.map_smul_univ] + sorry +/- lemma c2 [Fintype ι] (b : Basis ι ℝ E) @@ -79,7 +84,7 @@ lemma c2 intro i' rw [Orthonormal.inner_left_fintype hb] rw [Orthonormal.inner_left_fintype hb] - +-/ lemma fin_sum [Fintype ι] @@ -94,10 +99,8 @@ lemma fin_sum theorem LaplaceIndep [Fintype ι] [DecidableEq ι] - (v₁ : Basis ι ℝ E) - (hv₁ : Orthonormal ℝ v₁) - (v₂ : Basis ι ℝ E) - (hv₂ : Orthonormal ℝ v₂) + (v₁ : OrthonormalBasis ι ℝ E) + (v₂ : OrthonormalBasis ι ℝ E) (L : ContinuousMultilinearMap ℝ (fun (_ : Fin 2) ↩ E) F) : ∑ i, L (fun _ ↩ v₁ i) = ∑ i, L (fun _ => v₂ i) := by @@ -116,7 +119,7 @@ theorem LaplaceIndep right arg 2 intro i - rw [vectorPresentation v₁ hv₁ (v₂ i)] + rw [v₁.sum_repr' (v₂ i)] rw [BilinearCalc] rw [Finset.sum_comm] conv => @@ -160,10 +163,8 @@ noncomputable def Laplace_wrt_basis theorem LaplaceIndep' [Fintype ι] [DecidableEq ι] - (v₁ : Basis ι ℝ E) - (hv₁ : Orthonormal ℝ v₁) - (v₂ : Basis ι ℝ E) - (hv₂ : Orthonormal ℝ v₂) + (v₁ : OrthonormalBasis ι ℝ E) + (v₂ : OrthonormalBasis ι ℝ E) (f : E → F) : (Laplace_wrt_basis v₁ hv₁ f) = (Laplace_wrt_basis v₂ hv₂ f) := by diff --git a/lake-manifest.json b/lake-manifest.json index 67d262b..2f2d2de 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -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": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.36", "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": "9c4c6f78c9a1b7beba018504e284d497a3761af2", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index 9ad3040..e5ea660 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.9.0-rc3