Theorems · Theorem · complex analysis

AnalyticAt.exists_eq_sum_add_pow_mul

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {f : 𝕜 → E},
  AnalyticAt 𝕜 f 0 →
    ∀ (n : ℕ),
      ∃ F,
        AnalyticAt 𝕜 F 0 ∧
          ∀ (z : 𝕜), f z = ∑ i ∈ Finset.range n, (z ^ i / ↑i.factorial) • iteratedDeriv i f 0 + z ^ n • F z

A version of Taylor's theorem for analytic functions in one variable, with the error term of the form z ^ n times a function analytic at 0. (See AnalyticAt.exists_eventuallyEq_sum_add_pow_mul for a version asserting equality on a neighbourhood of 0 rather than globally.)

Defined in

Mathlib.Analysis.Analytic.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceCharZeroCompleteSpace