Update tensor.lean

Nevanlinna/bilinear.lean

@@ -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

Nevanlinna/laplace2.lean

@@ -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

Nevanlinna/tensor.lean

@@ -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

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",
+   "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed",
-   "name": "std",
+   "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,

lean-toolchain

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