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.laplace
import Nevanlinna.partialDeriv

variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]


def Harmonic (f : ℂ → 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 ℝ (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]

    -- This lemma says that partial derivatives commute with complex scalar
    -- multiplication. This is a consequence of partialDeriv_compContLin once we
    -- note that complex scalar multiplication is continuous ℝ-linear.
    have : ∀ v, ∀ s : ℂ, ∀ g : ℂ → ℂ, Differentiable ℝ g → partialDeriv ℝ v (s • g) = s • (partialDeriv ℝ v g) := by
      intro v s g hg

      -- Present scalar multiplication as a continuous ℝ-linear map. This is
      -- horrible, there must be better ways to do that.
      let sMuls : ℂ →L[ℝ] ℂ :=
      {
        toFun := fun x ↦ s * x
        map_add' := by
          intro x y
          ring
        map_smul' := by
          intro m x
          simp
          ring
      }

      -- Bring the goal into a form that is recognized by
      -- partialDeriv_compContLin.
      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


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)


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)