English
Let 𝕜 be a nontrivial normed field, E and F normed spaces, and s ⊆ E, t ⊆ E. For functions f, g : E → F and points x ∈ s, y ∈ t with unique differentiability at x and y, the distance between the first iterated derivatives of f and g within s and t equals the distance between their first derivatives within s and t, respectively.
Русский
Пусть 𝕜 — ненулевая нормированная поле, E и F — нормированные пространства, s ⊆ E, t ⊆ E. Пусть f, g : E → F и x ∈ s, y ∈ t такие, что в точках x и y выполняется уникальная дифференцируемость. Тогда расстояние между первыми обходными производными f и g внутри соответствующих множеств равно расстоянию между их производными внутри тех же множеств: dist(iteratedFDerivWithin 𝕜 1 f s x, iteratedFDerivWithin 𝕜 1 g t y) = dist(fderivWithin 𝕜 f s x, fderivWithin 𝕜 g t y).
LaTeX
$$$\operatorname{dist}\big( \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{(1)} f\,s\,x, \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^{(1)} g\,t\,y \big) = \operatorname{dist}\big( fderivWithin_{\mathbb{K}} f\,s\,x, fderivWithin_{\mathbb{K}} g\,t\,y \big)$$$
Lean4
@[simp]
theorem dist_iteratedFDerivWithin_one (f g : E → F) {y} (hsx : UniqueDiffWithinAt 𝕜 s x)
(hyt : UniqueDiffWithinAt 𝕜 t y) :
dist (iteratedFDerivWithin 𝕜 1 f s x) (iteratedFDerivWithin 𝕜 1 g t y) =
dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y) :=
by
simp only [iteratedFDerivWithin_succ_eq_comp_left, comp_apply, LinearIsometryEquiv.dist_map,
iteratedFDerivWithin_zero_eq_comp, LinearIsometryEquiv.comp_fderivWithin, hsx, hyt]
apply (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearIsometry.postcomp.dist_map
