Theorems · Theorem · complex analysis

analyticOrderAt_eq_nat_iff_iteratedDeriv_eq_zero

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CharZero 𝕜] [CompleteSpace E] {z₀ : 𝕜} {f : 𝕜 → E},
  AnalyticAt 𝕜 f z₀ →
    ∀ {n : ℕ}, analyticOrderAt f z₀ = ↑n ↔ (∀ k < n, iteratedDeriv k f z₀ = 0) ∧ iteratedDeriv n f z₀ ≠ 0

An analytic function f has finite analytic order n at z₀ if and only if its first n iterated derivatives (including f itself) vanish at z₀ and the n-th iterated derivative is non-zero.

Defined in

Mathlib.Analysis.Analytic.Order

Cited by

0 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpaceCharZeroCompleteSpace