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 Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
import Mathlib.Data.Complex.Module
import Mathlib.Data.Complex.Order
import Mathlib.Data.Complex.Exponential
import Mathlib.Data.Fin.Tuple.Basic
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)


theorem logabs_of_holomorphic_is_harmonic
  {f : ℂ → ℂ}
  (h₁ : Differentiable ℂ f)
  (h₂ : ∀ z, f z ≠ 0)
  (h₃ : ∀ z, f z ∈ Complex.slitPlane) :
  Harmonic (fun z ↦ Real.log ‖f z‖) := by

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

  -- The norm square is z * z.conj
  have normSq_conj : ∀ (z : ℂ), (starRingEnd ℂ) z * z = ↑‖z‖ ^ 2 := Complex.conj_mul'

  -- The norm square is real C²
  have normSq_is_real_C2 : ContDiff ℝ 2 Complex.normSq := by
    unfold Complex.normSq
    simp
    conv =>
      arg 3
      intro x
      rw [← Complex.reCLM_apply, ← Complex.imCLM_apply]
    apply ContDiff.add
    apply ContDiff.mul
    apply ContinuousLinearMap.contDiff Complex.reCLM
    apply ContinuousLinearMap.contDiff Complex.reCLM
    apply ContDiff.mul
    apply ContinuousLinearMap.contDiff Complex.imCLM
    apply ContinuousLinearMap.contDiff Complex.imCLM

  constructor
  · -- logabs f is real C²
    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
      funext z
      simp
      unfold Complex.abs
      simp
      rw [Real.log_sqrt]
      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
      exact Complex.normSq_nonneg (f z)
    rw [this]

    have : (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) = (fun z ↦ (2 : ℝ)⁻¹ • ((Real.log ∘ ⇑Complex.normSq ∘ f) z)) := by
      simp
    rw [this]

    apply contDiff_iff_contDiffAt.2
    intro z

    apply ContDiffAt.const_smul
    apply ContDiffAt.comp
    apply Real.contDiffAt_log.2
    simp
    exact h₂ z
    apply ContDiffAt.comp
    exact ContDiff.contDiffAt normSq_is_real_C2
    exact ContDiff.contDiffAt f_is_real_C2

  · -- Laplace vanishes
    have : (fun z ↦ Real.log ‖f z‖) = (2 : ℝ)⁻¹ • (Real.log ∘ Complex.normSq ∘ f) := by
      funext z
      simp
      unfold Complex.abs
      simp
      rw [Real.log_sqrt]
      rw [div_eq_inv_mul (Real.log (Complex.normSq (f z))) 2]
      exact Complex.normSq_nonneg (f z)
    rw [this]
    rw [laplace_smul]
    simp

    have : ∀ (z : ℂ), Complex.laplace (Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 ↔ Complex.laplace (Complex.ofRealCLM ∘ Real.log ∘ ⇑Complex.normSq ∘ f) z = 0 := by
      intro z
      rw [laplace_compContLin]
      simp
      sorry
    conv =>
      intro z
      rw [this z]

    have : Complex.ofRealCLM ∘ Real.log ∘ Complex.normSq ∘ f = Complex.log ∘ Complex.ofRealCLM ∘ Complex.normSq ∘ f := by
      unfold Function.comp
      funext z
      apply Complex.ofReal_log
      exact Complex.normSq_nonneg (f z)
    rw [this]

    have : Complex.ofRealCLM ∘ ⇑Complex.normSq ∘ f = ((starRingEnd ℂ) ∘ f) * f := by
      funext z
      simp
      exact Complex.normSq_eq_conj_mul_self
    rw [this]

    have : Complex.log ∘ (⇑(starRingEnd ℂ) ∘ f * f) = Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f + Complex.log ∘ f := by
      unfold Function.comp
      funext z
      simp
      rw [Complex.log_mul_eq_add_log_iff]

      have : Complex.arg ((starRingEnd ℂ) (f z)) = - Complex.arg (f z) := by
        rw [Complex.arg_conj]
        have : ¬ Complex.arg (f z) = Real.pi := by
          exact Complex.slitPlane_arg_ne_pi (h₃ z)
        simp
        tauto
      rw [this]
      simp
      constructor
      · exact Real.pi_pos
      · exact Real.pi_nonneg
      exact (AddEquivClass.map_ne_zero_iff starRingAut).mpr (h₂ z)
      exact h₂ z
    rw [this]
    rw [laplace_add]
    
    have : Differentiable ℂ (Complex.log ∘ f) := by
      intro z
      apply DifferentiableAt.comp 
      exact Complex.differentiableAt_log (h₃ z)
      exact h₁ z

    have : Complex.laplace (Complex.log ∘ f) = 0 := by
      let A := holomorphic_is_harmonic this
      funext z
      exact A.2 z
    rw [this]
    simp

    have : Complex.log ∘ ⇑(starRingEnd ℂ) ∘ f = ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f := by
      funext z
      unfold Function.comp
      rw [Complex.log_conj]
      exact Complex.slitPlane_arg_ne_pi (h₃ z)
    rw [this]

    have : ⇑(starRingEnd ℂ) ∘ Complex.log ∘ f = Complex.conjCLE ∘ Complex.log ∘ f := by
      rfl
    rw [this]
    have : ContDiff ℝ 2 (Complex.log ∘ f) := by sorry
    have : Complex.laplace (⇑Complex.conjCLE ∘ f) = ⇑Complex.conjCLE ∘ Complex.laplace (f) := by
      apply laplace_compContLin

      sorry
    rw [laplace_compContLin this]

    sorry

    sorry
    sorry