nevanlinna/nevanlinna/realHarmonic.lean

import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs

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₂₂

structure Harmonic (f : ℝ × ℝ → ℝ) : Prop where
  ker_Laplace : ∀ x, Real.laplace f x = 0
  cont_Diff : ContDiff ℝ 2 f