norm_iteratedFDeriv_comp_right — Mathlib

English

If g is a LinearIsometryEquiv, then the norm of iteratedFDerivWithin i (f ∘ g) equals the norm of iteratedFDerivWithin i f, on the corresponding domain.

Русский

Если g линейная изометрическая эквивалентность, норма iteratedFDerivWithin i (f ∘ g) равна норме iteratedFDerivWithin i f на правой области.

LaTeX

$$$\|iteratedFDerivWithin 𝕜 i (f \circ g) s x\| = \|iteratedFDerivWithin 𝕜 i f s (g x)\|$$$

Lean4

/-- Composition with a linear isometry on the right preserves the norm of the iterated derivative
within a set. -/
theorem norm_iteratedFDeriv_comp_right (g : G ≃ₗᵢ[𝕜] E) (f : E → F) (x : G) (i : ℕ) :
    ‖iteratedFDeriv 𝕜 i (f ∘ g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖ :=
  by
  simp only [← iteratedFDerivWithin_univ]
  apply g.norm_iteratedFDerivWithin_comp_right f uniqueDiffOn_univ (mem_univ (g x)) i

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