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 Nevanlinna.cauchyRiemann

noncomputable def Complex.laplace : (ℂ → ℂ) → (ℂ → ℂ) := by
  intro f

  let fx  := fun w ↦ (fderiv ℝ f w) 1
  let fxx := fun w ↦ (fderiv ℝ fx w) 1
  let fy  := fun w ↦ (fderiv ℝ f w) Complex.I
  let fyy := fun w ↦ (fderiv ℝ fy w) Complex.I
  exact fun z ↦ (fxx z) + (fyy z)


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

#check second_derivative_symmetric

lemma zwoDiff (f : ℝ × ℝ → ℝ) (h : ContDiff ℝ 2 f) : ∀ z a b : ℝ × ℝ, 0 = 1 := by
  intro z a b

  let fx  := fun w ↦ (fderiv ℝ f w) a
  let fxx := fun w ↦ (fderiv ℝ fx w) a
  let f2  := (fderiv ℝ (fun w => fderiv ℝ f w) z) a a

  have :  iteratedFDeriv ℝ 1 f z ![a] = 0 := by
    rw [iteratedFDeriv_succ_apply_left]
    simp
    let g := iteratedFDeriv ℝ 0 f
    simp at g
    sorry

  have : f2 = fxx z := by
    dsimp [f2, fxx, fx]

    sorry

  sorry


lemma derivSymm (f : ℂ → ℂ) (h : Differentiable ℝ f) :
  ∀ z a b : ℂ, (fderiv ℝ (fun w => fderiv ℝ f w) z) a b = (fderiv ℝ (fun w => fderiv ℝ f w) z) b a := by
  intro z a b

  let f' := fun w => (fderiv ℝ f w)
  have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
    exact fun y => DifferentiableAt.hasFDerivAt (h y)

  let f'' := (fderiv ℝ f' z)
  have h₁ : HasFDerivAt f' f'' z := by
    apply DifferentiableAt.hasFDerivAt
    sorry

  let A := second_derivative_symmetric h₀ h₁ a b
  dsimp [f'', f'] at A
  apply A

theorem re_comp_holomorphic_is_harmonic (f : ℂ → ℂ) :
  Differentiable ℂ f → Harmonic f := by

  intro h

  constructor
  · -- Complex.reCLM ∘ f is two times real continuously differentiable
    exact ContDiff.restrict_scalars ℝ (Differentiable.contDiff h)

  · -- Laplace of f is zero
    intro z
    unfold Complex.laplace

    simp

    conv =>
      left
      right
      arg 1
      arg 2
      intro z
      rw [CauchyRiemann₁ (h z)]

    have t₀ : ∀ z, DifferentiableAt ℝ (fun w => (fderiv ℝ f w) 1) z := by
      intro z

      sorry

    have t₁ : ∀ x, (fderiv ℝ (fun w => Complex.I * (fderiv ℝ f w) 1) z) x
      = Complex.I * ((fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) x) := by
      intro x
      rw [fderiv_const_mul]
      simp
      exact t₀ z
    rw [t₁]

    have t₂₀ : Differentiable ℝ f := by sorry
    have t₂ : (fderiv ℝ (fun w => (fderiv ℝ f w) 1) z) Complex.I
      = (fderiv ℝ (fun w => (fderiv ℝ f w) Complex.I) z) 1 := by
      let A := derivSymm f t₂₀ z 1 Complex.I

      sorry
    rw [t₂]

    conv =>
      left
      right
      arg 2
      arg 1
      arg 2
      intro z
      rw [CauchyRiemann₁ (h z)]

    rw [t₁]

    rw [← mul_assoc]
    simp