English
If g is a continuous linear equivalence, then ContDiff 𝕜 n f s is equivalent to ContDiff 𝕜 n (f ∘ g) on g⁻¹'(s) under appropriate change of variables.
Русский
Если g — непрерывная линейная эквивалентность, то дифференцируемость сохраняется под заменой переменных через композицию.
LaTeX
$$$\forall g:\, F \simeq_L G,\; ContDiffOn 𝕜 n (f\circ g) (g^{-1} s) \iff ContDiffOn 𝕜 n f s$$$
Lean4
/-- The iterated derivative within a set of the composition with a linear equiv on the right is
obtained by composing the iterated derivative with the linear equiv. -/
theorem iteratedFDerivWithin_comp_right (g : G ≃L[𝕜] 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)).compContinuousLinearMap fun _ => g :=
by
induction i generalizing x with ext1 m
| zero =>
simp only [iteratedFDerivWithin_zero_apply, comp_apply, ContinuousMultilinearMap.compContinuousLinearMap_apply]
| succ i
IH =>
simp only [ContinuousMultilinearMap.compContinuousLinearMap_apply, ContinuousLinearEquiv.coe_coe,
iteratedFDerivWithin_succ_apply_left]
have :
fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s)) (g ⁻¹' s) x =
fderivWithin 𝕜
(ContinuousLinearEquiv.continuousMultilinearMapCongrLeft _ (fun _x : Fin i => g) ∘
(iteratedFDerivWithin 𝕜 i f s ∘ g))
(g ⁻¹' s) x :=
fderivWithin_congr' (@IH) hx
rw [this, ContinuousLinearEquiv.comp_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx)]
simp only [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, comp_apply,
ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply,
ContinuousMultilinearMap.compContinuousLinearMap_apply]
rw [ContinuousLinearEquiv.comp_right_fderivWithin _ (g.uniqueDiffOn_preimage_iff.2 hs x hx),
ContinuousLinearMap.coe_comp', coe_coe, comp_apply, tail_def, tail_def]
