norm_iteratedFDeriv_comp_left — Mathlib

English

If g is a linear isometry equivalence, the left-norm of the i-th iterated derivative is preserved under g for all i within the domain context.

Русский

Если g — линейное изометрическое эквивалентное отображение, норма i-й итерационной производной сохраняется при применении g.

LaTeX

$$$\|D^i(g\circ f)(x)\| = \|D^i f(x)\|$ for all i$$

Lean4

/-- Composition with a linear isometry equiv on the left preserves the norm of the iterated
derivative. -/
theorem norm_iteratedFDeriv_comp_left (g : F ≃ₗᵢ[𝕜] G) (f : E → F) (x : E) (i : ℕ) :
    ‖iteratedFDeriv 𝕜 i (g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖ :=
  by
  rw [← iteratedFDerivWithin_univ, ← iteratedFDerivWithin_univ]
  apply g.norm_iteratedFDerivWithin_comp_left f uniqueDiffOn_univ (mem_univ x) i

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