From 5e3f9c463f150181fb588105a85b625bb4e694c5 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Mon, 13 May 2024 09:52:15 +0200 Subject: [PATCH] Update laplace.lean --- Nevanlinna/laplace.lean | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean index b708c98..2694a62 100644 --- a/Nevanlinna/laplace.lean +++ b/Nevanlinna/laplace.lean @@ -15,6 +15,7 @@ import Nevanlinna.cauchyRiemann import Nevanlinna.partialDeriv variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F] +variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G] noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) := @@ -43,7 +44,6 @@ theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁) (h₂ 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 intro v unfold Complex.laplace @@ -57,3 +57,18 @@ theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Compl exact h.differentiable one_le_two exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl exact h.differentiable one_le_two + + +theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) : + Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by + unfold Complex.laplace + rw [partialDeriv_compContLin] + rw [partialDeriv_compContLin] + rw [partialDeriv_compContLin] + rw [partialDeriv_compContLin] + simp + + exact (partialDeriv_contDiff ℝ h Complex.I).differentiable le_rfl + exact h.differentiable one_le_two + exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl + exact h.differentiable one_le_two