English
Under mild hypotheses, the i-th iterated derivative within s of g ∘ f equals the Taylor composition of g and f up to i.
Русский
При слабых гипотезах i-я итеративная производная внутри s от g ∘ f равна композиции Тейлора для g и f до i-й степени.
LaTeX
$$$\forall i,\; \operatorname{iteratedFDerivWithin} 𝕜 i (g \circ f) s x = (\ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (\ftaylorSeriesWithin 𝕜 f s x) i$$$
Lean4
theorem iteratedFDerivWithin_comp_of_eventually_mem {t : Set F} (hg : ContDiffWithinAt 𝕜 n g t (f x))
(hf : ContDiffWithinAt 𝕜 n f s x) (ht : UniqueDiffOn 𝕜 t) (hs : UniqueDiffOn 𝕜 s) (hxs : x ∈ s)
(hst : ∀ᶠ y in 𝓝[s] x, f y ∈ t) {i : ℕ} (hi : i ≤ n) :
iteratedFDerivWithin 𝕜 i (g ∘ f) s x =
(ftaylorSeriesWithin 𝕜 g t (f x)).taylorComp (ftaylorSeriesWithin 𝕜 f s x) i :=
by
obtain ⟨u, hxu, huo, hfu, hgu⟩ :
∃ u,
x ∈ u ∧
IsOpen u ∧
HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) (s ∩ u) ∧
HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' (s ∩ u)) :=
by
have hxt : f x ∈ t := hst.self_of_nhdsWithin hxs
have hf_tendsto : Tendsto f (𝓝[s] x) (𝓝[t] (f x)) := tendsto_nhdsWithin_iff.mpr ⟨hf.continuousWithinAt, hst⟩
have H₁ : ∀ᶠ u in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn i f (ftaylorSeriesWithin 𝕜 f s) u :=
hf.eventually_hasFTaylorSeriesUpToOn hs hxs hi
have H₂ : ∀ᶠ u in (𝓝[s] x).smallSets, HasFTaylorSeriesUpToOn i g (ftaylorSeriesWithin 𝕜 g t) (f '' u) :=
hf_tendsto.image_smallSets.eventually (hg.eventually_hasFTaylorSeriesUpToOn ht hxt hi)
rcases (nhdsWithin_basis_open _ _).smallSets.eventually_iff.mp (H₁.and H₂) with ⟨u, ⟨hxu, huo⟩, hu⟩
exact ⟨u, hxu, huo, hu (by simp [inter_comm])⟩
exact
.symm <|
(hgu.comp hfu (mapsTo_image _ _)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter huo)
⟨hxs, hxu⟩ |>.trans <|
iteratedFDerivWithin_inter_open huo hxu
