Theorems · Inductive type · real analysis

HasFTaylorSeriesUpToOn

{𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → (E → FormalMultilinearSeries 𝕜 E F) → Set E → Prop

HasFTaylorSeriesUpToOn n f p s registers the fact that p 0 = f and p (m+1) is a derivative of p m for m < n, and is continuous for m ≤ n. This is a predicate analogous to HasFDerivWithinAt but for higher-order derivatives. Notice that p does not sum up to f on the diagonal (FormalMultilinearSeries.sum), even if f is analytic and n = ∞: an additional 1/m! factor on the mth term is necessary for that.

Defined in

Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries

Cited by

80 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpace