tensorIteratedFDerivTwo — Mathlib

English

Equality between bilinearIteratedFDerivTwo 𝕜 f e and iteratedFDeriv 𝕜 2 f e.

Русский

Согласование между билинейной повторной производной и повторной производной второго порядка.

LaTeX

$$bilinearIteratedFDerivTwo_eq_iteratedFDeriv$$

Lean4

/-- Convenience reformulation of the second iterated derivative, as a map from `E` to linear maps
`E ⊗[𝕜] E →ₗ[𝕜] F`.
-/
noncomputable def tensorIteratedFDerivTwo (f : E → F) : E → E ⊗[𝕜] E →ₗ[𝕜] F := fun e ↦
  lift (bilinearIteratedFDerivTwo 𝕜 f e)

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