Nevanlinna/complexHarmonic.lean

@@ -85,30 +85,5 @@ 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,7 +15,6 @@ 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) :=
@@ -44,6 +43,7 @@ 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,18 +57,3 @@ 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