From 1c34aee7be3fa180a47c07b65806bd4722a4fc91 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 15 May 2024 15:31:57 +0200
Subject: [PATCH] working

---
 Nevanlinna/complexHarmonic.lean | 5 ++---
 Nevanlinna/laplace.lean         | 8 ++++++++
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 686ad1b..1f916e0 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -254,11 +254,10 @@ theorem logabs_of_holomorphic_is_harmonic
       rfl
     rw [this]
     have : ContDiff ℝ 2 (Complex.log ∘ f) := by sorry
-    have : Complex.laplace (⇑Complex.imCLM ∘ f) = ⇑Complex.imCLM ∘ Complex.laplace (f) := by
-      apply laplace_compContLin
 
+    have : Complex.laplace (⇑Complex.conjCLE ∘ f) = ⇑Complex.conjCLE ∘ Complex.laplace (f) := by
+      
       sorry
-    rw [laplace_compContLin this]
 
     sorry
 
diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index 2694a62..9d96a3c 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -72,3 +72,11 @@ theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff 
   exact h.differentiable one_le_two
   exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
   exact h.differentiable one_le_two
+
+
+theorem laplace_compCLE {f : ℂ → F} {l : F ≃L[ℝ] G} (h : ContDiff ℝ 2 f) :
+  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
+  let l' := (l : F →L[ℝ] G)
+  have : Complex.laplace (l' ∘ f) = l' ∘ (Complex.laplace f) := by
+    exact laplace_compContLin h
+  exact this