nevanlinna/Nevanlinna/partialDeriv.lean

import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.Calculus.FDeriv.Symmetric
import Mathlib.Analysis.Calculus.ContDiff.Basic


variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
variable (𝕜)


noncomputable def 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} : partialDeriv 𝕜 (a • v) f = a • partialDeriv 𝕜 v f := by
  unfold partialDeriv
  conv =>
    left
    intro w
    rw [map_smul]


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


theorem partialDeriv_smul₂ {f : E → F} {a : 𝕜} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (a • f) = a • partialDeriv 𝕜 v f := by
  unfold 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₂) : partialDeriv 𝕜 v (f₁ + f₂) = (partialDeriv 𝕜 v f₁) + (partialDeriv 𝕜 v f₂) := by
  unfold 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[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
  unfold partialDeriv

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


theorem partialDeriv_compContLinAt {f : E → F} {l : F →L[𝕜] G} {v : E} {x : E} (h : DifferentiableAt 𝕜 f x) : (partialDeriv 𝕜 v (l ∘ f)) x = (l ∘ partialDeriv 𝕜 v f) x:= by
  unfold partialDeriv
  rw [fderiv.comp x (ContinuousLinearMap.differentiableAt l) h]
  simp


theorem partialDeriv_contDiff {n : ℕ} {f : E → F} (h : ContDiff 𝕜 (n + 1) f) : ∀ v : E, ContDiff 𝕜 n (partialDeriv 𝕜 v f) := by
  unfold 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


theorem partialDeriv_contDiffAt {n : ℕ} {f : E → F} {x : E} (h : ContDiffAt 𝕜 (n + 1) f x) : ∀ v : E, ContDiffAt 𝕜 n (partialDeriv 𝕜 v f) x := by
  unfold partialDeriv
  intro v

  let A' := (contDiffAt_succ_iff_hasFDerivAt.1 h)
  obtain ⟨f', ⟨u, hu₁, hu₂⟩ , hf'⟩ := A'

  have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by
    rfl
  rw [this]
  apply ContDiffAt.comp
  apply fderiv_clm_apply

  let A := (contDiffAt_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 = partialDeriv 𝕜 b (partialDeriv 𝕜 a f) z := by

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


theorem partialDeriv_eventuallyEq {f₁ f₂ : E → F} {x : E} (h : f₁ =ᶠ[nhds x] f₂) : ∀ v : E, partialDeriv 𝕜 v f₁ x = partialDeriv 𝕜 v f₂ x := by
  unfold partialDeriv
  rw [Filter.EventuallyEq.fderiv_eq h]
  exact fun v => rfl


section restrictScalars

variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E]
variable [IsScalarTower 𝕜 𝕜' E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F]
variable [IsScalarTower 𝕜 𝕜' F]
--variable {f : E → F}

theorem partialDeriv_restrictScalars {f : E → F} {v : E} :
  Differentiable 𝕜' f → partialDeriv 𝕜 v f = partialDeriv 𝕜' v f := by
  intro hf
  unfold partialDeriv
  funext x
  rw [(hf x).fderiv_restrictScalars 𝕜]
  simp


theorem partialDeriv_comm
  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
  {f : E → F} (h : ContDiff ℝ 2 f) :
  ∀ v₁ v₂ : E, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) = partialDeriv ℝ v₂ (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₂]