nevanlinna/Nevanlinna/complexHarmonic.lean

import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Complex.TaylorSeries
import Mathlib.Analysis.Calculus.LineDeriv.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Nevanlinna.cauchyRiemann

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


def Harmonic (f : ℂ → ℝ) : Prop :=
  (ContDiff ℝ 2 f) ∧ (∀ z, Complex.laplace f z = 0)

#check contDiff_iff_ftaylorSeries.2

lemma c2_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℂ 2 f := by
  intro fHyp
  exact Differentiable.contDiff fHyp

lemma c2R_if_holomorphic (f : ℂ → ℂ) : Differentiable ℂ f → ContDiff ℝ 2 f := by
  intro fHyp
  let ZZ := c2_if_holomorphic f fHyp
  apply ContDiff.restrict_scalars ℝ ZZ



theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
  Differentiable ℂ f → Harmonic (Complex.reCLM ∘ f) := by

  intro h

  constructor
  · -- Complex.reCLM ∘ f is two times real continuously differentiable
    apply ContDiff.comp
    · -- Complex.reCLM is two times real continuously differentiable
      exact ContinuousLinearMap.contDiff Complex.reCLM
    · -- f is two times real continuously differentiable
      exact c2R_if_holomorphic f h

  · -- Laplace of f is zero
    intro z
    unfold Complex.laplace
    simp
    let ZZ := (CauchyRiemann₃ (h z)).left

    sorry