Update partialDeriv.lean

This commit is contained in:
Stefan Kebekus 2024-05-30 09:57:36 +02:00
parent 3bdc7eaffb
commit f480ae2a0f
1 changed files with 12 additions and 17 deletions

View File

@ -91,30 +91,25 @@ theorem partialDeriv_contDiff {n : } {f : E → F} (h : ContDiff 𝕜 (n + 1)
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'
let eval_at_v : (E →L[𝕜] F) →L[𝕜] F :=
{
toFun := fun l ↦ l v
map_add' := by simp
map_smul' := by simp
}
have : (fun w => (fderiv 𝕜 f w) v) = (fun f => f v) ∘ (fun w => (fderiv 𝕜 f w)) := by
have : (fun w => (fderiv 𝕜 f w) v) = eval_at_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
apply ContDiffAt.continuousLinearMap_comp
-- ContDiffAt 𝕜 (↑n) (fun w => fderiv 𝕜 f w) x
apply ContDiffAt.fderiv_right h
rfl
lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) :