tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin

English

Relation between tensorized second iterated derivative within and iteratedFDerivWithin.

Русский

Связь между тензорной формой второго повторного производного внутри и iteratedFDerivWithin.

LaTeX

$$tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin f hs he e1 e2$$

Lean4

/-- Expression of `tensorIteratedFDerivTwo` in terms of `iteratedFDerivWithin`.
-/
theorem tensorIteratedFDerivWithinTwo_eq_iteratedFDerivWithin {e : E} {s : Set E} (f : E → F) (hs : UniqueDiffOn 𝕜 s)
    (he : e ∈ s) (e₁ e₂ : E) :
    tensorIteratedFDerivWithinTwo 𝕜 f s e (e₁ ⊗ₜ[𝕜] e₂) = iteratedFDerivWithin 𝕜 2 f s e ![e₁, e₂] := by
  rw [← bilinearIteratedFDerivWithinTwo_eq_iteratedFDeriv f hs he, tensorIteratedFDerivWithinTwo, lift.tmul]

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