Update complexHarmonic.lean

Nevanlinna/complexHarmonic.lean

@@ -85,5 +85,30 @@ theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
 theorem re_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ f) :
   Harmonic (Complex.reCLM ∘ f) := by
 
+  constructor
+  · -- Continuous differentiability
+    apply ContDiff.comp
+    exact ContinuousLinearMap.contDiff Complex.reCLM
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+  · rw [laplace_compContLin]
+    simp
+    intro z
+    rw [(holomorphic_is_harmonic h).right z]
+    simp
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
 
-  sorry
+
+theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ}  (h : Differentiable ℂ f) :
+  Harmonic (Complex.imCLM ∘ f) := by
+
+  constructor
+  · -- Continuous differentiability
+    apply ContDiff.comp
+    exact ContinuousLinearMap.contDiff Complex.imCLM
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)
+  · rw [laplace_compContLin]
+    simp
+    intro z
+    rw [(holomorphic_is_harmonic h).right z]
+    simp
+    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)

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