From e5f25514827a2dc93fa7631584d25c810715398c Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 13 May 2024 09:48:16 +0200 Subject: [PATCH] Fix error --- Nevanlinna/laplace.lean | 5 +++++ Nevanlinna/partialDeriv.lean | 3 ++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index d26026a..b708c98 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -37,6 +37,11 @@ theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ exact (partialDeriv_contDiff ℝ h₂ Complex.I).differentiable le_rfl exact h₁.differentiable one_le_two exact h₂.differentiable one_le_two + exact (partialDeriv_contDiff ℝ h₁ 1).differentiable le_rfl + exact (partialDeriv_contDiff ℝ h₂ 1).differentiable le_rfl + exact h₁.differentiable one_le_two + exact h₂.differentiable one_le_two + theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index 47d6596..6e73723 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -6,6 +6,7 @@ import Mathlib.Analysis.Calculus.ContDiff.Basic variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] +variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G] variable (𝕜) @@ -53,7 +54,7 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable rw [fderiv_add (h₁ w) (h₂ w)] -theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] F} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by +theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by unfold partialDeriv conv =>