contDiffWithinAt_comp_iff — Mathlib

English

Composition with a linear isometry on the right preserves the norm of the iterated derivative.

Русский

Композиция справа линейной изометрии сохраняет норму итеративной производной.

LaTeX

$$$\|iteratedFDeriv 𝕜^i (f\circ g) x\| = \|iteratedFDeriv 𝕜^i f (g x)\|$$$

Lean4

/-- Composition by continuous linear equivs on the right respects higher differentiability at a
point in a domain. -/
theorem contDiffWithinAt_comp_iff (e : G ≃L[𝕜] E) :
    ContDiffWithinAt 𝕜 n (f ∘ e) (e ⁻¹' s) (e.symm x) ↔ ContDiffWithinAt 𝕜 n f s x :=
  by
  constructor
  · intro H
    simpa [← preimage_comp, Function.comp_def] using H.comp_continuousLinearMap (e.symm : E →L[𝕜] G)
  · intro H
    rw [← e.apply_symm_apply x, ← e.coe_coe] at H
    exact H.comp_continuousLinearMap _

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