Vanishing Order of Analytic Functions

This file defines the order of vanishing of an analytic function f at a point z₀, as an element of ℕ∞.

TODO: Uniformize API between analytic and meromorphic functions

Vanishing Order at a Point: Definition and Characterization

noncomputable def AnalyticAt.order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : ℕ∞

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.order_eq_top_iff and AnalyticAt.order_eq_nat_iff for these equivalences.

Equations

• hf.order = if h : ∀ᶠ (z : 𝕜) in nhds z₀, f z = 0 then ⊤ else ↑⋯.choose

theorem AnalyticAt.order_eq_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : hf.order = ⊤ ↔ ∀ᶠ (z : 𝕜) in nhds z₀, f z = 0

The order of an analytic function f at a z₀ is infinity iff f vanishes locally around z₀.

theorem AnalyticAt.order_eq_nat_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {n : ℕ} (hf : AnalyticAt 𝕜 f z₀) : hf.order = ↑n ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z

The order of an analytic function f at z₀ equals a natural number n iff f can locally be written as f z = (z - z₀) ^ n • g z, where g is analytic and does not vanish at z₀.

theorem AnalyticAt.order_ne_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : hf.order ≠ ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[nhds z₀] fun (z : 𝕜) => (z - z₀) ^ hf.order.toNat • g z

The order of an analytic function f at z₀ is finite iff f can locally be written as f z = (z - z₀) ^ order • g z, where g is analytic and does not vanish at z₀.

See MeromorphicNFAt.order_eq_zero_iff for an analogous statement about meromorphic functions in normal form.

@[deprecated AnalyticAt.order_ne_top_iff (since := "2025-02-03")]

theorem AnalyticAt.order_neq_top_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : hf.order ≠ ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[nhds z₀] fun (z : 𝕜) => (z - z₀) ^ hf.order.toNat • g z

Alias of AnalyticAt.order_ne_top_iff.

---

The order of an analytic function f at z₀ is finite iff f can locally be written as f z = (z - z₀) ^ order • g z, where g is analytic and does not vanish at z₀.

See MeromorphicNFAt.order_eq_zero_iff for an analogous statement about meromorphic functions in normal form.

theorem AnalyticAt.order_eq_zero_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : hf.order = 0 ↔ f z₀ ≠ 0

The order of an analytic function f at z₀ is zero iff f does not vanish at z₀.

theorem AnalyticAt.apply_eq_zero_of_order_toNat_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : hf.order.toNat ≠ 0 → f z₀ = 0

An analytic function vanishes at a point if its order is nonzero when converted to ℕ.

Vanishing Order at a Point: Behaviour under Ring Operations

The theorem AnalyticAt.order_mul and AnalyticAt.order_pow establish additivity of the order under multiplication and taking powers.

TODO: Behaviour under Addition/Subtraction

theorem AnalyticAt.order_mul_of_order_eq_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {f g : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) (h'f : hf.order = ⊤) : ⋯.order = ⊤

Helper lemma for AnalyticAt.order_mul

theorem AnalyticAt.order_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {f g : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) : ⋯.order = hf.order + hg.order

The order is additive when multiplying analytic functions.

theorem AnalyticAt.order_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {f : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀) {n : ℕ} : ⋯.order = n • hf.order

The order multiplies by n when taking an analytic function to its nth power.

Level Sets of the Order Function

theorem AnalyticOnNhd.isClopen_setOf_order_eq_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) : IsClopen {u : ↑U | ⋯.order = ⊤}

The set where an analytic function has infinite order is clopen in its domain of analyticity.

theorem AnalyticOnNhd.exists_order_ne_top_iff_forall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsConnected U) : (∃ (u : ↑U), ⋯.order ≠ ⊤) ↔ ∀ (u : ↑U), ⋯.order ≠ ⊤

On a connected set, there exists a point where a meromorphic function f has finite order iff f has finite order at every point.

theorem AnalyticOnNhd.order_ne_top_of_isPreconnected {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) {x y : 𝕜} (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : ⋯.order ≠ ⊤) : ⋯.order ≠ ⊤

On a preconnected set, a meromorphic function has finite order at one point if it has finite order at another point.

theorem AnalyticOnNhd.codiscrete_setOf_order_eq_zero_or_top {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} (hf : AnalyticOnNhd 𝕜 f U) : {u : ↑U | ⋯.order = 0 ∨ ⋯.order = ⊤} ∈ Filter.codiscrete ↑U

The set where an analytic function has zero or infinite order is discrete within its domain of analyticity.