Theorems · Theorem · real analysis

norm_iteratedFDerivWithin_comp_le

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type uG}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {n : ℕ} {s : Set E} {t : Set F}
  {x : E} {N : WithTop ℕ∞},
  ContDiffOn 𝕜 N g t →
    ContDiffOn 𝕜 N f s →
      ↑n ≤ N →
        UniqueDiffOn 𝕜 t →
          UniqueDiffOn 𝕜 s →
            Set.MapsTo f s t →
              x ∈ s →
                ∀ {C D : ℝ},
                  (∀ i ≤ n, ‖iteratedFDerivWithin 𝕜 i g t (f x)‖ ≤ C) →
                    (∀ (i : ℕ), 1 ≤ i → i ≤ n → ‖iteratedFDerivWithin 𝕜 i f s x‖ ≤ D ^ i) →
                      ‖iteratedFDerivWithin 𝕜 n (g ∘ f) s x‖ ≤ ↑n.factorial * C * D ^ n

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.

Defined in

Mathlib.Analysis.Calculus.ContDiff.Bounds

Cited by

1 results in Mathlib

Foundations

Depth 204 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace