nevanlinna/complexHarmonic.lean

@@ -1,39 +0,0 @@
-import Mathlib.Analysis.Complex.Basic
-import Mathlib.Analysis.Calculus.LineDeriv.Basic
-import Mathlib.Analysis.Calculus.ContDiff.Defs
-import Mathlib.Analysis.Calculus.FDeriv.Basic
-
-noncomputable def Real.laplace : (ℝ × ℝ → ℝ) → (ℝ × ℝ → ℝ) := by
-  intro f
-  let f₁ := fun x ↦ lineDeriv ℝ f x ⟨1,0⟩
-  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x ⟨1,0⟩
-  let f₂ := fun x ↦ lineDeriv ℝ f x ⟨0,1⟩
-  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x ⟨0,1⟩
-  exact f₁₁ + f₂₂
-
-noncomputable def Complex.laplace : (ℂ → ℝ) → (ℂ → ℝ) := by
-  intro f
-  let f₁ := fun x ↦ lineDeriv ℝ f x 1
-  let f₁₁ := fun x ↦ lineDeriv ℝ f₁ x 1
-  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
-  let f₂₂ := fun x ↦ lineDeriv ℝ f₂ x Complex.I
-  exact f₁₁ + f₂₂
-
-
-theorem xx : ∀ f : ℂ → , f = 0  := by
-  intro f
-
-  let f₁ := fun x ↦ lineDeriv ℝ f x 1
-  let f₂ := fun x ↦ lineDeriv ℝ f x Complex.I
-
-  have : ∀ z, fderiv ℂ f z = 0 := by
-    sorry
-
-
-  have : (fun x ↦ lineDeriv ℝ f x 1) = (fun x ↦ lineDeriv ℝ f x Complex.I) := by
-
-    unfold lineDeriv
-
-    sorry
-
-  sorry

nevanlinna/realHarmonic.lean

@@ -11,6 +11,6 @@ noncomputable def Real.laplace : (ℝ × ℝ → ℝ) → (ℝ × ℝ → ℝ) :
 
   exact f₁₁ + f₂₂
 
-
-def Harmonic (f : ℝ × ℝ → ℝ) : Prop :=
-  (ContDiff ℝ 2 f) ∧ (∀ x, Real.laplace f x = 0)
+structure Harmonic (f : ℝ × ℝ → ℝ) : Prop where
+  ker_Laplace : ∀ x, Real.laplace f x = 0
+  cont_Diff : ContDiff ℝ 2 f