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 ℕ.

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

Characterization of which natural numbers are ≤ hf.order. Useful for avoiding case splits, since it applies whether or not the order is ∞.

theorem AnalyticAt.order_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {z₀ : 𝕜} (hf₁ : AnalyticAt 𝕜 f₁ z₀) (h : f₁ =ᶠ[nhds z₀] f₂) : ⋯.order = hf₁.order

If two functions agree in a neighborhood of z₀, then their orders at z₀ agree.

Vanishing Order at a Point: Elementary Computations

theorem AnalyticAt.analyticAt_centeredMonomial {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] (z₀ : 𝕜) (n : ℕ) : AnalyticAt 𝕜 ((fun (x : 𝕜) => x - z₀) ^ n) z₀

Helper lemma, required to state analyticAt_order_centeredMonomial below

@[simp]

theorem AnalyticAt.analyticAt_order_centeredMonomial {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {n : ℕ} : ⋯.order = ↑n

Simplifier lemma for the order of a centered monomial

Vanishing Order at a Point: Behaviour under Standard Operations

The theorems AnalyticAt.order_mul and AnalyticAt.order_pow establish additivity of the order under multiplication and taking powers. The theorem AnalyticAt.order_add establishes behavior under addition.

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

The order is additive when scalar multiplying analytic functions.

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.

theorem AnalyticAt.order_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {z₀ : 𝕜} (hf₁ : AnalyticAt 𝕜 f₁ z₀) (hf₂ : AnalyticAt 𝕜 f₂ z₀) : min hf₁.order hf₂.order ≤ ⋯.order

The order of a sum is at least the minimum of the orders of the summands.

theorem AnalyticAt.order_add_of_order_lt_order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {z₀ : 𝕜} (hf₁ : AnalyticAt 𝕜 f₁ z₀) (hf₂ : AnalyticAt 𝕜 f₂ z₀) (h : hf₁.order < hf₂.order) : ⋯.order = hf₁.order

Helper lemma for AnalyticAt.order_add_of_unequal_order

theorem AnalyticAt.order_add_of_order_ne_order {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f₁ f₂ : 𝕜 → E} {z₀ : 𝕜} (hf₁ : AnalyticAt 𝕜 f₁ z₀) (hf₂ : AnalyticAt 𝕜 f₂ z₀) (h : hf₁.order ≠ hf₂.order) : ⋯.order = min hf₁.order hf₂.order

If two functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.

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.