Theorems · Definition · complex analysis

analyticOrderNatAt

{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → 𝕜 → ℕ

The order of vanishing of f at z₀, as an element of ℕ. The order is defined to be 0 if f is identically zero on a neighbourhood of z₀, and is otherwise the unique n such that f can locally be written as f z = (z - z₀) ^ n • g z, where g is analytic and does not vanish at z₀. See AnalyticAt.analyticOrderAt_eq_top and AnalyticAt.analyticOrderAt_eq_natCast for these equivalences. If f isn't analytic at z₀, then analyticOrderNatAt f z₀ returns a junk value of 0.

Defined in

Mathlib.Analysis.Analytic.Order

Cited by

9 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace