Theorems · Definition · complex analysis

analyticOrderAt

{𝕜 : 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 ∞ if f is identically 0 on a neighbourhood of z₀, and 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 analyticOrderAt f z₀ returns a junk value of 0.

Defined in

Mathlib.Analysis.Analytic.Order

Cited by

69 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldNormedAddCommGroupNormedSpace