Theorems · Theorem · real analysis

ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear_aux

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {Du Eu Fu Gu : Type u} [inst_1 : NormedAddCommGroup Du]
  [inst_2 : NormedSpace 𝕜 Du] [inst_3 : NormedAddCommGroup Eu] [inst_4 : NormedSpace 𝕜 Eu]
  [inst_5 : NormedAddCommGroup Fu] [inst_6 : NormedSpace 𝕜 Fu] [inst_7 : NormedAddCommGroup Gu]
  [inst_8 : NormedSpace 𝕜 Gu] (B : Eu →L[𝕜] Fu →L[𝕜] Gu) {f : Du → Eu} {g : Du → Fu} {n : ℕ} {s : Set Du} {x : Du},
  ContDiffOn 𝕜 (↑n) f s →
    ContDiffOn 𝕜 (↑n) g s →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          ‖iteratedFDerivWithin 𝕜 n (fun y => (B (f y)) (g y)) s x‖ ≤
            ‖B‖ *
              ∑ i ∈ Finset.range (n + 1),
                ↑(n.choose i) * ‖iteratedFDerivWithin 𝕜 i f s x‖ * ‖iteratedFDerivWithin 𝕜 (n - i) g s x‖

Bounding the norm of the iterated derivative of B (f x) (g x) within a set in terms of the iterated derivatives of f and g when B is bilinear. This lemma is an auxiliary version assuming all spaces live in the same universe, to enable an induction. Use instead ContinuousLinearMap.norm_iteratedFDerivWithin_le_of_bilinear that removes this assumption.

Defined in

Mathlib.Analysis.Calculus.ContDiff.Bounds

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace