Theorems · Theorem · real analysis

FormalMultilinearSeries.taylorComp_sub_taylorComp_isBigO

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {α : Type u_5} {H : Type u_6}
  [inst_7 : NormedAddCommGroup H] {l : Filter α} {p₁ p₂ : α → FormalMultilinearSeries 𝕜 F G}
  {q₁ q₂ : α → FormalMultilinearSeries 𝕜 E F} {f : α → H} {n : ℕ},
  (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖p₁ x k‖) →
    (∀ k ≤ n, (fun a => p₁ a k - p₂ a k) =O[l] f) →
      (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖q₁ x k‖) →
        (∀ k ≤ n, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖q₂ x k‖) →
          (∀ k ≤ n, (fun a => q₁ a k - q₂ a k) =O[l] f) →
            (fun a => (p₁ a).taylorComp (q₁ a) n - (p₂ a).taylorComp (q₂ a) n) =O[l] f

An upper estimate (in terms of Asymptotics.IsBigO) on the difference between two compositions of Taylor series. Let p₁, p₂, q₁, q₂ be four families of formal multilinear series depending on a parameter a. Suppose that the norms of (p₁ · k), (q₁ · k), and (q₂ · k) are bounded along a filter l for all k ≤ n. Also, suppose that $p₁(a, k) - p₂(a, k) = O(f(a))$, $q₁(a, k) - q₂(a, k) = O(f(a))$ along l for all k ≤ n. Then the difference between nth terms of (p₁ a).taylorComp (q₁ a) and (p₂ a).taylorComp (q₂ a) is O(f(a)) too. This lemma can be used, e.g., to show that the composition of two $C^{k+α}$ functions is a $C^{k+α}$ function.

Defined in

Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceNormedAddCommGroup