English
An auxiliary bound used in high-order derivative estimates for compositions.
Русский
Вспомогательное неравенство для оценки высших производных композиции.
LaTeX
$$$\displaystyle \|\operatorname{iteratedFDerivWithin}_{\mathbb{k}} n (g \circ f) s x\| \le n! \cdot C \\cdot D^n$$$
Lean4
/-- If the derivatives within a set of `g` at `f x` are bounded by `C`, and the `i`-th derivative
within a set of `f` at `x` is bounded by `D^i` for all `1 ≤ i ≤ n`, then the `n`-th derivative
of `g ∘ f` is bounded by `n! * C * D^n`. -/
theorem norm_iteratedFDerivWithin_comp_le {g : F → G} {f : E → F} {n : ℕ} {s : Set E} {t : Set F} {x : E}
{N : WithTop ℕ∞} (hg : ContDiffOn 𝕜 N g t) (hf : ContDiffOn 𝕜 N f s) (hn : n ≤ N) (ht : UniqueDiffOn 𝕜 t)
(hs : UniqueDiffOn 𝕜 s) (hst : MapsTo f s t) (hx : x ∈ s) {C : ℝ} {D : ℝ}
(hC : ∀ i, i ≤ n → ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C)
(hD : ∀ i, 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) :
‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ n ! * C * D ^ n := by
/- We reduce the bound to the case where all spaces live in the same universe (in which we
already have proved the result), by using linear isometries between the spaces and their `ULift`
to a common universe. These linear isometries preserve the norm of the iterated derivative. -/
let Fu : Type max uF uG := ULift.{uG, uF} F
let Gu : Type max uF uG := ULift.{uF, uG} G
have isoF : Fu ≃ₗᵢ[𝕜] F := LinearIsometryEquiv.ulift 𝕜 F
have isoG : Gu ≃ₗᵢ[𝕜] G := LinearIsometryEquiv.ulift 𝕜 G
let fu : E → Fu := isoF.symm ∘ f
let gu : Fu → Gu := isoG.symm ∘ g ∘ isoF
let tu := isoF ⁻¹' t
have htu : UniqueDiffOn 𝕜 tu := isoF.toContinuousLinearEquiv.uniqueDiffOn_preimage_iff.2 ht
have hstu : MapsTo fu s tu := fun y hy ↦ by
simpa only [fu, tu, mem_preimage, comp_apply, LinearIsometryEquiv.apply_symm_apply] using hst hy
have Ffu : isoF (fu x) = f x := by
simp only [fu, comp_apply, LinearIsometryEquiv.apply_symm_apply]
-- All norms are preserved by the lifting process.
have hfu : ContDiffOn 𝕜 n fu s := isoF.symm.contDiff.comp_contDiffOn (hf.of_le hn)
have hgu : ContDiffOn 𝕜 n gu tu :=
isoG.symm.contDiff.comp_contDiffOn ((hg.of_le hn).comp_continuousLinearMap (isoF : Fu →L[𝕜] F))
have Nfu : ∀ i, ‖iteratedFDerivWithin 𝕜 i fu s x‖ = ‖iteratedFDerivWithin 𝕜 i f s x‖ := fun i ↦ by
rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]
simp_rw [← Nfu] at hD
have Ngu : ∀ i, ‖iteratedFDerivWithin 𝕜 i gu tu (fu x)‖ = ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ := fun i ↦
by
rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ htu (hstu hx)]
rw [LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_right _ _ ht, Ffu]
rw [Ffu]
exact hst hx
simp_rw [← Ngu] at hC
have Nfgu : ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ = ‖iteratedFDerivWithin 𝕜 n (gu ∘ fu) s x‖ :=
by
have : gu ∘ fu = isoG.symm ∘ g ∘ f := by
ext x
simp only [fu, gu, comp_apply, LinearIsometryEquiv.apply_symm_apply]
rw [this, LinearIsometryEquiv.norm_iteratedFDerivWithin_comp_left _ _ hs hx]
-- deduce the required bound from the one for `gu ∘ fu`.
rw [Nfgu]
exact norm_iteratedFDerivWithin_comp_le_aux hgu hfu htu hs hstu hx hC hD
