nevanlinna/Nevanlinna/complexHarmonic.lean

import Mathlib.Data.Fin.Tuple.Basic
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 Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Data.Complex.Module
import Mathlib.Data.Complex.Order
import Mathlib.Data.Complex.Exponential
import Mathlib.Analysis.RCLike.Basic
import Mathlib.Topology.Algebra.InfiniteSum.Module
import Mathlib.Topology.Instances.RealVectorSpace
import Nevanlinna.cauchyRiemann
import Nevanlinna.partialDeriv


noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
  intro f
  let fx  := Real.partialDeriv 1 f
  let fxx := Real.partialDeriv 1 fx
  let fy  := Real.partialDeriv Complex.I f
  let fyy := Real.partialDeriv Complex.I fy
  exact fxx + fyy


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


theorem holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
  Harmonic f := by

  -- f is real C²
  have f_is_real_C2 : ContDiff ℝ 2 f :=
    ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)

  have fI_is_real_differentiable : Differentiable ℝ (Real.partialDeriv 1 f) := by
    exact (partialDeriv_contDiff f_is_real_C2 1).differentiable (Submonoid.oneLE.proof_2 ℕ∞)

  constructor
  · -- f is two times real continuously differentiable
    exact f_is_real_C2

  · -- Laplace of f is zero
    unfold Complex.laplace
    rw [CauchyRiemann₄ h]

    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g →  Real.partialDeriv v (s • g) = s • (Real.partialDeriv v g) := by
      intro v s g hg

      let sMuls : ℂ →L[ℝ] ℂ :=
      {
        toFun := fun x ↦ s * x
        map_add' := by
          intro x y
          ring
        map_smul' := by
          intro m x
          simp
          ring
      }

      have : s • g = sMuls ∘ g := by rfl
      rw [this]
      rw [partialDeriv_compContLin hg]
      rfl

    rw [this]
    rw [partialDeriv_comm f_is_real_C2 Complex.I 1]
    rw [CauchyRiemann₄ h]
    rw [this]
    rw [← smul_assoc]
    simp

    -- Subgoals coming from the application of 'this'
    -- Differentiable ℝ (Real.partialDeriv 1 f)
    exact fI_is_real_differentiable
    -- Differentiable ℝ (Real.partialDeriv 1 f)
    exact fI_is_real_differentiable