From c785a85f26443b7207ac5e5e37e3b521fe72270a Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 25 Jul 2024 15:52:16 +0200 Subject: [PATCH] Make things compile again --- Nevanlinna/bilinear.lean | 17 +---- Nevanlinna/cauchyRiemann.lean | 10 +-- Nevanlinna/complexHarmonic.lean | 2 +- Nevanlinna/holomorphic.lean | 3 +- Nevanlinna/laplace2.lean | 23 ++---- Nevanlinna/partialDeriv.lean | 6 ++ Nevanlinna/smulImprovement.lean | 40 ---------- Nevanlinna/tensor.lean | 47 ------------ Nevanlinna/test.lean | 130 -------------------------------- lake-manifest.json | 25 +++--- lean-toolchain | 2 +- 11 files changed, 40 insertions(+), 265 deletions(-) delete mode 100644 Nevanlinna/smulImprovement.lean delete mode 100644 Nevanlinna/tensor.lean delete mode 100644 Nevanlinna/test.lean diff --git a/Nevanlinna/bilinear.lean b/Nevanlinna/bilinear.lean index 1ed7b86..dacf4c4 100644 --- a/Nevanlinna/bilinear.lean +++ b/Nevanlinna/bilinear.lean @@ -32,24 +32,13 @@ 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 : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : E ⊗[ℝ] E := ∑ i, ((stdOrthonormalBasis ℝ E) i) ⊗ₜ[ℝ] ((stdOrthonormalBasis ℝ E) i) @@ -64,9 +53,9 @@ theorem InnerProductSpace.canonicalCovariantTensorRepresentation right arg 2 intro i - rw [w.sum_repr' (v 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] diff --git a/Nevanlinna/cauchyRiemann.lean b/Nevanlinna/cauchyRiemann.lean index 1884075..9a839b1 100644 --- a/Nevanlinna/cauchyRiemann.lean +++ b/Nevanlinna/cauchyRiemann.lean @@ -45,8 +45,8 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z) theorem CauchyRiemann₄ - {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] - {f : ℂ → F} : + {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] + {f : ℂ → F} : (Differentiable ℂ f) → partialDeriv ℝ Complex.I f = Complex.I • partialDeriv ℝ 1 f := by intro h unfold partialDeriv @@ -58,13 +58,13 @@ theorem CauchyRiemann₄ simp rw [← mul_one Complex.I] rw [← smul_eq_mul] - rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f w) Complex.I 1] conv => right right intro w rw [DifferentiableAt.fderiv_restrictScalars ℝ (h w)] - + funext w + simp theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] {f : ℂ → F} {z : ℂ} : (DifferentiableAt ℂ f z) → partialDeriv ℝ Complex.I f z = Complex.I • partialDeriv ℝ 1 f z := by @@ -77,8 +77,8 @@ theorem CauchyRiemann₅ {F : Type*} [NormedAddCommGroup F] [NormedSpace ℂ F] simp rw [← mul_one Complex.I] rw [← smul_eq_mul] - rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1] conv => right right rw [DifferentiableAt.fderiv_restrictScalars ℝ h] + simp diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean index d604f03..a24a32f 100644 --- a/Nevanlinna/complexHarmonic.lean +++ b/Nevanlinna/complexHarmonic.lean @@ -33,7 +33,7 @@ theorem HarmonicAt_iff · constructor · exact Set.mem_inter h₂s₁ h₃s₂ · constructor - · exact h₃s₁.mono (Set.inter_subset_left s₁ s₂) + · exact h₃s₁.mono Set.inter_subset_left · intro z hz exact h₂t₂ (h₁s₂ hz.2) · intro hyp diff --git a/Nevanlinna/holomorphic.lean b/Nevanlinna/holomorphic.lean index e4eb207..eed131c 100644 --- a/Nevanlinna/holomorphic.lean +++ b/Nevanlinna/holomorphic.lean @@ -137,12 +137,11 @@ theorem CauchyRiemann'₅ simp rw [← mul_one Complex.I] rw [← smul_eq_mul] - rw [ContinuousLinearMap.map_smul_of_tower (fderiv ℂ f z) Complex.I 1] conv => right right rw [DifferentiableAt.fderiv_restrictScalars ℝ h] - + simp theorem CauchyRiemann'₆ {f : ℂ → F} diff --git a/Nevanlinna/laplace2.lean b/Nevanlinna/laplace2.lean index cf95e5a..c641bae 100644 --- a/Nevanlinna/laplace2.lean +++ b/Nevanlinna/laplace2.lean @@ -10,15 +10,6 @@ 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] @@ -27,20 +18,20 @@ noncomputable def realInnerAsElementOfDualTensorprod : TensorProduct ℝ E E →ₗ[ℝ] ℝ := TensorProduct.lift bilinFormOfRealInner -instance +instance {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] - : NormedAddCommGroup (TensorProduct ℝ E E) where - norm := by - + : NormedAddCommGroup (TensorProduct ℝ E E) where + norm := by + sorry - dist_self := by - + dist_self := by + sorry sorry /- -instance +instance {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [FiniteDimensional ℝ E] : InnerProductSpace ℝ (TensorProduct ℝ E E) where smul := _ diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index d0395b8..020aca4 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -44,6 +44,8 @@ theorem partialDeriv_smul₁ {f : E → F} {a : 𝕜} {v : E} : partialDeriv left intro w rw [map_smul] + funext w + simp theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v₁ + v₂) f = (partialDeriv 𝕜 v₁ f) + (partialDeriv 𝕜 v₂ f) := by @@ -52,6 +54,8 @@ theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : partialDeriv 𝕜 (v left intro w rw [map_add] + funext w + simp theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by @@ -90,6 +94,8 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} (h₁ : Differentiable 𝕜 f intro w left rw [fderiv_add (h₁ w) (h₂ w)] + funext w + simp theorem partialDeriv_add₂_differentiableAt diff --git a/Nevanlinna/smulImprovement.lean b/Nevanlinna/smulImprovement.lean deleted file mode 100644 index 573f49c..0000000 --- a/Nevanlinna/smulImprovement.lean +++ /dev/null @@ -1,40 +0,0 @@ -import Mathlib.Analysis.Complex.CauchyIntegral ---import Mathlib.Analysis.Complex.Module - - - -example simplificationTest₁ - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E] - {v : E} - {z : ℂ} : - z • v = z.re • v + Complex.I • z.im • v := by - - /- - An attempt to write "rw [add_smul]" will fail with "did not find instance of - the pattern in the target -- expression (?r + ?s) • ?x". - -/ - sorry - - -theorem add_smul' - (𝕜₁ : Type*) [NontriviallyNormedField ℝ] - {𝕜₂ : Type*} [NontriviallyNormedField ℂ] [NormedAlgebra ℝ ℂ] - {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] [IsScalarTower ℝ ℂ E] - {v : E} - {r s : ℂ} : - (r + s) • v = r • v + s • v := - Module.add_smul r s v - - -theorem smul_add' (a : M) (b₁ b₂ : A) : a • (b₁ + b₂) = a • b₁ + a • b₂ := - DistribSMul.smul_add _ _ _ -#align smul_add smul_add - - - - -example simplificationTest₂ - {v : E} - {z : ℂ} : - z • v = z.re • v + Complex.I • z.im • v := by - sorry diff --git a/Nevanlinna/tensor.lean b/Nevanlinna/tensor.lean deleted file mode 100644 index f805778..0000000 --- a/Nevanlinna/tensor.lean +++ /dev/null @@ -1,47 +0,0 @@ -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 \ No newline at end of file diff --git a/Nevanlinna/test.lean b/Nevanlinna/test.lean deleted file mode 100644 index 966fde2..0000000 --- a/Nevanlinna/test.lean +++ /dev/null @@ -1,130 +0,0 @@ -import Mathlib.Analysis.Complex.CauchyIntegral ---import Mathlib.Analysis.Complex.Module --- test - -open ComplexConjugate - -#check DiffContOnCl.circleIntegral_sub_inv_smul - -open Real - -theorem CauchyIntegralFormula : - ∀ - {R : ℝ} -- Radius of the ball - {w : ℂ} -- Point in the interior of the ball - {f : ℂ → ℂ}, -- Holomorphic function - DiffContOnCl ℂ f (Metric.ball 0 R) - → w ∈ Metric.ball 0 R - → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * π * Complex.I) • f w := by - - exact DiffContOnCl.circleIntegral_sub_inv_smul - -#check CauchyIntegralFormula -#check HasDerivAt.continuousAt -#check Real.log -#check ComplexConjugate.conj -#check Complex.exp - -theorem SimpleCauchyFormula : - ∀ - {R : ℝ} -- Radius of the ball - {w : ℂ} -- Point in the interior of the ball - {f : ℂ → ℂ}, -- Holomorphic function - Differentiable ℂ f - → w ∈ Metric.ball 0 R - → (∮ (z : ℂ) in C(0, R), (z - w)⁻¹ • f z) = (2 * Real.pi * Complex.I) • f w := by - - intro R w f fHyp - - apply DiffContOnCl.circleIntegral_sub_inv_smul - - constructor - · exact Differentiable.differentiableOn fHyp - · suffices Continuous f from by - exact Continuous.continuousOn this - rw [continuous_iff_continuousAt] - intro x - exact DifferentiableAt.continuousAt (fHyp x) - - -theorem JensenFormula₂ : - ∀ - {R : ℝ} -- Radius of the ball - {f : ℂ → ℂ}, -- Holomorphic function - Differentiable ℂ f - → (∀ z ∈ Metric.ball 0 R, f z ≠ 0) - → (∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ‖f (circleMap 0 R θ)‖ ) = 2 * π * Complex.log ‖f 0‖ := by - - intro r f fHyp₁ fHyp₂ - - /- We treat the trivial case r = 0 separately. -/ - by_cases rHyp : r = 0 - rw [rHyp] - simp - left - unfold ENNReal.ofReal - simp - rw [max_eq_left (mul_nonneg zero_le_two pi_nonneg)] - simp - /- From hereon, we assume that r ≠ 0. -/ - - /- Replace the integral over 0 … 2π by a circle integral -/ - suffices (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) = 2 * ↑π * Complex.log ↑‖f 0‖ from by - have : ∫ (θ : ℝ) in Set.Icc 0 (2 * π), Complex.log ↑‖f (circleMap 0 r θ)‖ = (∮ (z : ℂ) in C(0, r), -(Complex.I * z⁻¹ * Complex.log ↑(Complex.abs (f z)))) := by - have : (fun θ ↦ Complex.log ‖f (circleMap 0 r θ)‖) = (fun θ ↦ ((deriv (circleMap 0 r) θ)) • ((deriv (circleMap 0 r) θ)⁻¹ • Complex.log ↑‖f (circleMap 0 r θ)‖)) := by - funext θ - rw [← smul_assoc, smul_eq_mul, smul_eq_mul, mul_inv_cancel, one_mul] - simp - exact rHyp - rw [this] - simp - let tmp := circleIntegral_def_Icc (fun z ↦ -(Complex.I * z⁻¹ * (Complex.log ↑‖f z‖))) 0 r - simp at tmp - rw [← tmp] - rw [this] - - - - have : ∀ z : ℂ, log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by - intro z - - by_cases argHyp : Complex.arg z = π - - · rw [Complex.log, argHyp, Complex.log] - let ZZ := Complex.arg_conj z - rw [argHyp] at ZZ - - simp at ZZ - - have : conj z = z := by - apply? - sorry - - let ZZ := Complex.log_conj z - - nth_rewrite 1 [Complex.log] - - simp - - let φ := Complex.arg z - let r := Complex.abs z - have : z = r * Complex.exp (φ * Complex.I) := by - exact (Complex.abs_mul_exp_arg_mul_I z).symm - - have : Complex.log z = Complex.log r + r*Complex.I := by - apply? - sorry - simp at XX - - - sorry - - - - - - - - - - sorry diff --git a/lake-manifest.json b/lake-manifest.json index bbb73cc..7830064 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,10 +1,11 @@ -{"version": "1.0.0", +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "555ec79bc6effe7009036184a5f73f7d8d4850ed", + "scope": "leanprover-community", + "rev": "d2b1546c5fc05a06426e3f6ee1cb020e71be5592", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -13,7 +14,8 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", + "scope": "leanprover-community", + "rev": "01ad33937acd996ee99eb74eefb39845e4e4b9f5", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,7 +24,8 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "30619d94ce4a3d69cdb87bb1771562ca2e687cfa", + "scope": "leanprover-community", + "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -31,25 +34,28 @@ {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9", + "scope": "leanprover-community", + "rev": "d1b33202c3a29a079f292de65ea438648123b635", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.38", + "inputRev": "v0.0.39", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, + "scope": "", "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/import-graph.git", + {"url": "https://github.com/leanprover-community/import-graph", "type": "git", "subDir": null, - "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96", + "scope": "leanprover-community", + "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +64,8 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "dcc73cfb2ce3763f830c52042fb8617e762dbf60", + "scope": "", + "rev": "cc495260156b40dcbd55b947c047061e15344000", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/lean-toolchain b/lean-toolchain index e5ea660..6a4259f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0-rc3 +leanprover/lean4:v4.10.0-rc2