Theorems · Theorem · real analysis

norm_iteratedFDerivWithin_comp_le_aux

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {Fu Gu : Type u} [inst_3 : NormedAddCommGroup Fu] [inst_4 : NormedSpace 𝕜 Fu]
  [inst_5 : NormedAddCommGroup Gu] [inst_6 : NormedSpace 𝕜 Gu] {g : Fu → Gu} {f : E → Fu} {n : ℕ} {s : Set E}
  {t : Set Fu} {x : E},
  ContDiffOn 𝕜 (↑n) g t →
    ContDiffOn 𝕜 (↑n) f s →
      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. This lemma proves this estimate assuming additionally that two of the spaces live in the same universe, to make an induction possible. Use instead norm_iteratedFDerivWithin_comp_le that removes this assumption.

Defined in

Mathlib.Analysis.Calculus.ContDiff.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace