iteratedPDeriv_eq_iteratedFDeriv — Mathlib

English

For any n, the iterated partial derivative of a Schwartz map coincides with the classical iterated Fréchet derivative: iteratedPDeriv 𝕜 m f x = iteratedFDeriv ℝ n f x m.

Русский

Для любого n итерационная частная производная совпадает с классическим итерационным пределом Фреше: iteratedPDeriv 𝕜 m f x = iteratedFDeriv ℝ n f x m.

LaTeX

$$$iteratedPDeriv 𝕜\, m\, f x = iteratedFDeriv ℝ n f x\, m$$$

Lean4

theorem iteratedPDeriv_eq_iteratedFDeriv {n : ℕ} {m : Fin n → E} {f : 𝓢(E, F)} {x : E} :
    iteratedPDeriv 𝕜 m f x = iteratedFDeriv ℝ n f x m := by
  induction n generalizing x with
  | zero => simp
  | succ n ih =>
    simp only [iteratedPDeriv_succ_left, iteratedFDeriv_succ_apply_left]
    rw [← fderiv_continuousMultilinear_apply_const_apply]
    · simp [← ih]
    · exact (f.smooth ⊤).differentiable_iteratedFDeriv (mod_cast ENat.coe_lt_top n) x

Похожие утверждения