English
If g is a linear isometry equivalence, the norm of the i-th iterated derivative of f is preserved under left composition by g.
Русский
Если g линейная изометрическая эквивалентность, норма i-й итеративной производной f сохраняется при левой композиции.
LaTeX
$$$\|\operatorname{iteratedFDeriv}_{\mathbb{K}}^i (g\circ f)(x)\| = \|\operatorname{iteratedFDeriv}_{\mathbb{K}}^i f(x)\|$$$
Lean4
/-- Composition with a linear isometry on the right preserves the norm of the iterated derivative
within a set. -/
theorem norm_iteratedFDerivWithin_comp_right (g : G ≃ₗᵢ[𝕜] E) (f : E → F) (hs : UniqueDiffOn 𝕜 s) {x : G} (hx : g x ∈ s)
(i : ℕ) : ‖iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x‖ = ‖iteratedFDerivWithin 𝕜 i f s (g x)‖ :=
by
have :
iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x =
(iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g :=
g.toContinuousLinearEquiv.iteratedFDerivWithin_comp_right f hs hx i
rw [this, ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv]
