nevanlinna/Nevanlinna/partialDeriv.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.Basic
import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric


noncomputable def Real.partialDeriv : ℂ → (ℂ → ℂ) → (ℂ → ℂ) := by
  intro v
  intro f
  exact fun w ↦ (fderiv ℝ f w) v


theorem partialDeriv_smul {f : ℂ → ℂ } {a v : ℂ} (h : Differentiable ℝ f) : Real.partialDeriv v (a • f) = a • Real.partialDeriv v f := by
  unfold Real.partialDeriv

  have : a • f = fun y ↦ a • f y := by rfl
  rw [this]

  conv =>
    left
    intro w
    rw [fderiv_const_smul (h w)]


theorem partialDeriv_contDiff {n : ℕ} {f : ℂ → ℂ} (h : ContDiff ℝ (n + 1) f) : ∀ v : ℂ, ContDiff ℝ n (Real.partialDeriv v f) := by
  unfold Real.partialDeriv
  intro v

  let A := (contDiff_succ_iff_fderiv.1 h).right
  simp at A

  have : (fun w => (fderiv ℝ f w) v) = (fun f => f v) ∘ (fun w => (fderiv ℝ f w)) := by
    rfl

  rw [this]
  refine ContDiff.comp ?hg A
  refine ContDiff.of_succ ?hg.h
  refine ContDiff.clm_apply ?hg.h.hf ?hg.h.hg
  exact contDiff_id
  exact contDiff_const


lemma l₂ {f : ℂ → ℂ} (hf : ContDiff ℝ 2 f) (z a b : ℂ) :
    fderiv ℝ (fderiv ℝ f) z b a = fderiv ℝ (fun w ↦ fderiv ℝ f w a) z b := by
  rw [fderiv_clm_apply]
  · simp
  · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
  · simp


lemma derivSymm (f : ℂ → ℂ) (hf : ContDiff ℝ 2 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' := fderiv ℝ f
  have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
    have h : Differentiable ℝ f := by
      exact (contDiff_succ_iff_fderiv.1 hf).left
    exact fun y => DifferentiableAt.hasFDerivAt (h y)

  let f'' := (fderiv ℝ f' z)
  have h₁ : HasFDerivAt f' f'' z := by
    apply DifferentiableAt.hasFDerivAt
    let A := (contDiff_succ_iff_fderiv.1 hf).right
    let B := (contDiff_succ_iff_fderiv.1 A).left
    simp at B
    exact B z

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


theorem partialDeriv_comm {f : ℂ → ℂ} (h : ContDiff ℝ 2 f) :
  ∀ v₁ v₂ : ℂ, Real.partialDeriv v₁ (Real.partialDeriv v₂ f) = Real.partialDeriv v₂ (Real.partialDeriv v₁ f) := by

  intro v₁ v₂
  unfold Real.partialDeriv
  funext z

  conv =>
    left
    rw [← l₂ h z v₂ v₁]

  rw [derivSymm f h z v₁ v₂]

  conv =>
    left
    rw [l₂ h z v₁ v₂]