From 9a9fbf1b549a636283d57aafffb0b2d552544d5f Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Fri, 28 Jun 2024 07:53:20 +0200 Subject: [PATCH] Update mathlib --- Nevanlinna/bilinear.lean | 181 +++++++++++++++++++++++++++++++++------ Nevanlinna/laplace2.lean | 2 +- lake-manifest.json | 6 +- 3 files changed, 161 insertions(+), 28 deletions(-) diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean index 7f6f5fe..54869fc 100644 --- a/Nevanlinna/bilinear.lean +++ b/Nevanlinna/bilinear.lean @@ -1,4 +1,4 @@ -import Mathlib.Algebra.BigOperators.Basic +--import Mathlib.Algebra.BigOperators.Basic import Mathlib.Analysis.InnerProductSpace.Basic import Mathlib.Analysis.InnerProductSpace.Dual import Mathlib.Analysis.InnerProductSpace.PiL2 @@ -9,31 +9,164 @@ open Finset variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] - -open TensorProduct - -example : 0 = 1 := by - - let B := (sesqFormOfInner (𝕜 := ℝ) (E := E)).flip - - - have e: E := by sorry - let C := B e - - let α := InnerProductSpace.toDual ℝ E - - let β : E →ₗ[ℝ] ℝ := by sorry - let YY := E ⊗[ℝ] E - - let ZZ := TensorProduct.mapBilinear ℝ E E ℝ ℝ - - - let A : E × E → LinearMap.BilinForm ℝ E := by - unfold LinearMap.BilinForm - intro (e₁, e₂) +open BigOperators +open Finset - sorry +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 ι] + (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 + + 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 + + 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 diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean index 7597bac..cdc5023 100644 --- a/Nevanlinna/laplace2.lean +++ b/Nevanlinna/laplace2.lean @@ -1,7 +1,7 @@ import Mathlib.Analysis.InnerProductSpace.Basic import Mathlib.Analysis.InnerProductSpace.Dual import Mathlib.Analysis.InnerProductSpace.PiL2 -import Mathlib.Algebra.BigOperators.Basic +--import Mathlib.Algebra.BigOperators.Basic import Mathlib.Analysis.Calculus.ContDiff.Bounds import Mathlib.Analysis.Calculus.FDeriv.Symmetric import Mathlib.LinearAlgebra.Basis diff --git a/lake-manifest.json b/lake-manifest.json index 2f2d2de..bbb73cc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -31,10 +31,10 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", + "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.36", + "inputRev": "v0.0.38", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "9c4c6f78c9a1b7beba018504e284d497a3761af2", + "rev": "dcc73cfb2ce3763f830c52042fb8617e762dbf60", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,