English
For a fixed g, the i-th iterated derivative of the composition g ∘ f at x is the left composition of g with the i-th iterated derivative of f at x.
Русский
Для фиксированного g i-я итерационная производная композиции g ∘ f равна левой композиции g с i-й производной f.
LaTeX
$$$\forall f, g, x, i:\; iteratedFDeriv_{\mathbb{K}}^i (g\circ f)(x) = g\circ (iteratedFDeriv_{\mathbb{K}}^i f)(x)$$$
Lean4
/-- Composition with a linear isometry on the left preserves the norm of the iterated
derivative within a set. -/
theorem norm_iteratedFDerivWithin_comp_left {f : E → F} (g : F →ₗᵢ[𝕜] G) (hf : ContDiffWithinAt 𝕜 n f s x)
(hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {i : ℕ} (hi : i ≤ n) :
‖iteratedFDerivWithin 𝕜 i (g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖ :=
by
have :
iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
g.toContinuousLinearMap.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
g.toContinuousLinearMap.iteratedFDerivWithin_comp_left hf hs hx hi
rw [this]
apply LinearIsometry.norm_compContinuousMultilinearMap
