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.Comp
import Mathlib.Analysis.Calculus.FDeriv.Linear
import Mathlib.Analysis.Calculus.FDeriv.Symmetric

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

noncomputable def Real.partialDeriv : E → (E → F) → (E → F) :=
  fun v ↦ (fun f ↦ (fun w ↦ fderiv ℝ f w v))


theorem partialDeriv_smul₁ {f : E → F} {a : ℝ} {v : E} : Real.partialDeriv (a • v) f = a • Real.partialDeriv v f := by
  unfold Real.partialDeriv
  conv =>
    left
    intro w
    rw [map_smul]


theorem partialDeriv_add₁ {f : E → F} {v₁ v₂ : E} : Real.partialDeriv (v₁ + v₂) f = (Real.partialDeriv v₁ f) + (Real.partialDeriv v₂ f) := by
  unfold Real.partialDeriv
  conv =>
    left
    intro w
    rw [map_add]


theorem partialDeriv_smul₂ {f : E → F} {a : ℝ} {v : E} (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_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable ℝ f₁)  (h₂ : Differentiable ℝ f₂) : Real.partialDeriv v (f₁ + f₂) = (Real.partialDeriv v f₁) + (Real.partialDeriv v f₂) := by
  unfold Real.partialDeriv

  have : f₁ + f₂ = fun y ↦ f₁ y + f₂ y := by rfl
  rw [this]
  conv =>
    left
    intro w
    left
    rw [fderiv_add (h₁ w) (h₂ w)]


theorem partialDeriv_compContLin {f : E → F} {l : F →L[ℝ] F} {v : E} (h : Differentiable ℝ f) : Real.partialDeriv v (l ∘ f) = l ∘ Real.partialDeriv v f := by
  unfold Real.partialDeriv

  conv =>
    left
    intro w
    left
    rw [fderiv.comp w (ContinuousLinearMap.differentiableAt l) (h w)]
  simp
  rfl


theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff ℝ (n + 1) f) : ∀ v : E, 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 partialDeriv_fderiv {f : E → F} (hf : ContDiff ℝ 2 f) (z a b : E) :
    fderiv ℝ (fderiv ℝ f) z b a = Real.partialDeriv b (Real.partialDeriv a f) z := by

  unfold Real.partialDeriv
  rw [fderiv_clm_apply]
  · simp
  · exact (contDiff_succ_iff_fderiv.1 hf).2.differentiable le_rfl z
  · simp


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

  intro v₁ v₂
  funext z

  have derivSymm :
    (fderiv ℝ (fun w => fderiv ℝ f w) z) v₁ v₂ = (fderiv ℝ (fun w => fderiv ℝ f w) z) v₂ v₁ := by

    let f' := fderiv ℝ f
    have h₀ : ∀ y, HasFDerivAt f (f' y) y := by
      intro y
      exact DifferentiableAt.hasFDerivAt ((h.differentiable one_le_two) y)

    let f'' := (fderiv ℝ f' z)
    have h₁ : HasFDerivAt f' f'' z := by
      apply DifferentiableAt.hasFDerivAt
      apply (contDiff_succ_iff_fderiv.1 h).right.differentiable (Submonoid.oneLE.proof_2 ℕ∞)

    apply second_derivative_symmetric h₀ h₁ v₁ v₂


  rw [← partialDeriv_fderiv h z v₂ v₁]
  rw [derivSymm]
  rw [partialDeriv_fderiv h z v₁ v₂]