norm_iteratedFDeriv_comp_left — Mathlib

English

If g is a linear isometry, then the norm of the i-th iterated derivative is preserved under left composition by g: ∥D^i(g ∘ f)∥ = ∥D^i f∥.

Русский

Если g — линейная изометрия, то норма i-й итеративной производной сохраняется при левой композиции: ∥D^i(g∘f)∥ = ∥D^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 left preserves the norm of the iterated
derivative. -/
theorem norm_iteratedFDeriv_comp_left {f : E → F} (g : F →ₗᵢ[𝕜] G) (hf : ContDiffAt 𝕜 n f x) {i : ℕ} (hi : i ≤ n) :
    ‖iteratedFDeriv 𝕜 i (g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖ :=
  by
  simp only [← iteratedFDerivWithin_univ]
  exact g.norm_iteratedFDerivWithin_comp_left hf.contDiffWithinAt uniqueDiffOn_univ (mem_univ x) hi

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