From a15d473434914f3efe300130295ea1939b8ec70b Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Wed, 5 Jun 2024 16:31:55 +0200
Subject: [PATCH] Update partialDeriv.lean

---
 Nevanlinna/partialDeriv.lean | 65 ++++++++++++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)

diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 19d4bed..33f3aec 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -226,6 +226,33 @@ lemma partialDeriv_fderivOn
   · simp
 
 
+lemma partialDeriv_fderivAt
+  {z : E}
+  {f : E → F}
+  (hf : ContDiffAt 𝕜 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
+
+  -- DifferentiableAt 𝕜 (fun w => fderiv 𝕜 f w) z
+  obtain ⟨f', ⟨u, h₁u, h₂u⟩, hf' ⟩ := contDiffAt_succ_iff_hasFDerivAt.1 hf
+  have t₁ : (fun w ↦ fderiv 𝕜 f w) =ᶠ[nhds z] f' := by
+    apply Filter.eventuallyEq_iff_exists_mem.2
+    use u
+    constructor
+    · exact h₁u
+    · intro x hx
+      exact HasFDerivAt.fderiv (h₂u x hx)
+  rw [Filter.EventuallyEq.differentiableAt_iff t₁]
+  exact hf'.differentiableAt le_rfl
+
+  -- DifferentiableAt 𝕜 (fun w => a) z
+  exact differentiableAt_const a
+
+
 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]
@@ -356,3 +383,41 @@ theorem partialDeriv_commOn
   rw [← partialDeriv_fderivOn ℝ hs h v₂ v₁ z hz]
   rw [derivSymm]
   rw [← partialDeriv_fderivOn ℝ hs h v₁ v₂ z hz]
+
+
+theorem partialDeriv_commAt
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+  {z : E}
+  {f : E → F}
+  (h : ContDiffAt ℝ 2 f z) :
+  ∀ v₁ v₂ : E, partialDeriv ℝ v₁ (partialDeriv ℝ v₂ f) z = partialDeriv ℝ v₂ (partialDeriv ℝ v₁ f) z := by
+
+  intro v₁ v₂
+
+  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 ∈ s, HasFDerivAt f (f' y) y := by
+      intro y hy
+      apply DifferentiableAt.hasFDerivAt
+      apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hy)
+      apply h.differentiableOn one_le_two
+
+    let f'' := (fderiv ℝ f' z)
+    have h₁ : HasFDerivAt f' f'' z := by
+      apply DifferentiableAt.hasFDerivAt
+      apply DifferentiableOn.differentiableAt _ (IsOpen.mem_nhds hs hz)
+      apply ContDiffOn.differentiableOn _ (Submonoid.oneLE.proof_2 ℕ∞)
+      exact ((contDiffOn_succ_iff_fderiv_of_isOpen hs).1 h).2
+
+    have h₀' : ∀ᶠ (y : E) in nhds z, HasFDerivAt f (f' y) y := by
+      apply eventually_nhds_iff.mpr
+      use s
+
+    exact second_derivative_symmetric_of_eventually h₀' h₁ v₁ v₂
+
+  rw [← partialDeriv_fderivAt ℝ hs h v₂ v₁ z hz]
+  rw [derivSymm]
+  rw [← partialDeriv_fderivOn ℝ hs h v₁ v₂ z hz]