hasFDerivAt_expMap — Mathlib

English

Let K be a number field with its real embedding space. The exponential map expMap : realSpace(K) → realSpace(K) is Frechet-differentiable at every point x, and its derivative is the linear map fderiv_expMap at x.

Русский

Пусть K — число поле с вещественным пространством реализаций. Экспоненциальное отображение expMap: realSpace(K) → realSpace(K) дифференцируемо по Фредхету в каждой точке x, производная равна линейному отображению fderiv_expMap в точке x.

LaTeX

$$$D\expMap(x) = \mathrm{fderiv\_expMap}(x)$$$

Lean4

theorem hasFDerivAt_expMap (x : realSpace K) : HasFDerivAt expMap (fderiv_expMap x) x := by
  simpa [expMap, fderiv_expMap, hasFDerivAt_pi', OpenPartialHomeomorph.pi_apply, ContinuousLinearMap.proj_pi] using
    fun w ↦ (hasDerivAt_expMap_single w _).hasFDerivAt.comp x (hasFDerivAt_apply w x)

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