working

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
 

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