English
For a linear isometry equivalence g, the iterated derivative within a set s of g ∘ f equals g applied to the iterated derivative within s of f, and this holds uniformly for all i.
Русский
Для линейного изометрического эквивалента g итеративная производная внутри s от g ∘ f равна g применению к итеративной производной внутри s от f для всех i.
LaTeX
$$$\forall g:\, F \simeq F',\; \operatorname{iteratedFDerivWithin}_{\mathbb{K}}^i(g\circ f) \, s \, x = g\circ (\operatorname{iteratedFDerivWithin}_{\mathbb{K}}^i f \, s \, x)$$$
Lean4
/-- Composition with a linear isometry equiv on the left preserves the norm of the iterated
derivative within a set. -/
theorem norm_iteratedFDerivWithin_comp_left (g : F ≃ₗᵢ[𝕜] G) (f : E → F) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) (i : ℕ) :
‖iteratedFDerivWithin 𝕜 i (g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖ :=
by
have :
iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
(g : F →L[𝕜] G).compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) :=
g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_left f hs hx i
rw [this]
apply LinearIsometry.norm_compContinuousMultilinearMap g.toLinearIsometry
