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 analyticOrderAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (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.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.

Equations

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

noncomputable def analyticOrderNatAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (f : 𝕜 → E) (z₀ : 𝕜) : ℕ

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.

Equations

• analyticOrderNatAt f z₀ = (analyticOrderAt f z₀).toNat

@[simp]

theorem analyticOrderAt_of_not_analyticAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : ¬AnalyticAt 𝕜 f z₀) : analyticOrderAt f z₀ = 0

@[simp]

theorem analyticOrderNatAt_of_not_analyticAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : ¬AnalyticAt 𝕜 f z₀) : analyticOrderNatAt f z₀ = 0

@[simp]

theorem Nat.cast_analyticOrderNatAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : analyticOrderAt f z₀ ≠ ⊤) : ↑(analyticOrderNatAt f z₀) = analyticOrderAt f z₀

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

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

theorem AnalyticAt.analyticOrderAt_eq_natCast {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {n : ℕ} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : analyticOrderAt f z₀ = ↑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.analyticOrderNatAt_eq_iff {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hf' : analyticOrderAt f z₀ ≠ ⊤) {n : ℕ} : analyticOrderNatAt f z₀ = 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.analyticOrderAt_ne_top {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) : analyticOrderAt f z₀ ≠ ⊤ ↔ ∃ (g : 𝕜 → E), AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ f =ᶠ[nhds z₀] fun (z : 𝕜) => (z - z₀) ^ analyticOrderNatAt f z₀ • g z

The order of an analytic function f at z₀ is finite iff f can locally be written as f z = (z - z₀) ^ analyticOrderNatAt f z₀ • 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 analyticOrderAt_eq_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} : analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0

theorem analyticOrderAt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} : analyticOrderAt f z₀ ≠ 0 ↔ AnalyticAt 𝕜 f z₀ ∧ f z₀ = 0

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

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

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

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

theorem apply_eq_zero_of_analyticOrderAt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : analyticOrderAt f z₀ ≠ 0) : f z₀ = 0

A function vanishes at a point if its analytic order is nonzero in ℕ∞.

theorem apply_eq_zero_of_analyticOrderNatAt_ne_zero {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : analyticOrderNatAt f z₀ ≠ 0) : f z₀ = 0

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

theorem natCast_le_analyticOrderAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) {n : ℕ} : ↑n ≤ analyticOrderAt f z₀ ↔ ∃ (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 analyticOrderAt_congr {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} (hfg : f =ᶠ[nhds z₀] g) : analyticOrderAt f z₀ = analyticOrderAt g z₀

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

@[simp]

theorem analyticOrderAt_neg {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} : analyticOrderAt (-f) z₀ = analyticOrderAt f z₀

theorem le_analyticOrderAt_add {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} : min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀

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

theorem le_analyticOrderAt_sub {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} : min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f - g) z₀

theorem analyticOrderAt_add_eq_left_of_lt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} (hfg : analyticOrderAt f z₀ < analyticOrderAt g z₀) : analyticOrderAt (f + g) z₀ = analyticOrderAt f z₀

theorem analyticOrderAt_add_eq_right_of_lt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} (hgf : analyticOrderAt g z₀ < analyticOrderAt f z₀) : analyticOrderAt (f + g) z₀ = analyticOrderAt g z₀

theorem analyticOrderAt_add_of_ne {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜} (hfg : analyticOrderAt f z₀ ≠ analyticOrderAt g z₀) : analyticOrderAt (f + g) z₀ = min (analyticOrderAt f z₀) (analyticOrderAt g z₀)

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

theorem analyticOrderAt_smul_eq_top_of_left {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {z₀ : 𝕜} {f : 𝕜 → 𝕜} (hf : analyticOrderAt f z₀ = ⊤) : analyticOrderAt (f • g) z₀ = ⊤

theorem analyticOrderAt_smul_eq_top_of_right {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {z₀ : 𝕜} {f : 𝕜 → 𝕜} (hg : analyticOrderAt g z₀ = ⊤) : analyticOrderAt (f • g) z₀ = ⊤

theorem analyticOrderAt_smul {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {g : 𝕜 → E} {z₀ : 𝕜} {f : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) : analyticOrderAt (f • g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

The order is additive when scalar multiplying analytic functions.

Vanishing Order at a Point: Elementary Computations

@[simp]

theorem analyticOrderAt_centeredMonomial {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {n : ℕ} : analyticOrderAt ((fun (x : 𝕜) => x - z₀) ^ n) z₀ = ↑n

Simplifier lemma for the order of a centered monomial

theorem analyticOrderAt_mul_eq_top_of_left {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜} (hf : analyticOrderAt f z₀ = ⊤) : analyticOrderAt (f * g) z₀ = ⊤

theorem analyticOrderAt_mul_eq_top_of_right {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜} (hg : analyticOrderAt g z₀ = ⊤) : analyticOrderAt (f * g) z₀ = ⊤

theorem analyticOrderAt_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) : analyticOrderAt (f * g) z₀ = analyticOrderAt f z₀ + analyticOrderAt g z₀

The order is additive when multiplying analytic functions.

theorem analyticOrderNatAt_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f g : 𝕜 → 𝕜} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) (hf' : analyticOrderAt f z₀ ≠ ⊤) (hg' : analyticOrderAt g z₀ ≠ ⊤) : analyticOrderNatAt (f * g) z₀ = analyticOrderNatAt f z₀ + analyticOrderNatAt g z₀

The order is additive when multiplying analytic functions.

theorem analyticOrderAt_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) (n : ℕ) : analyticOrderAt (f ^ n) z₀ = n • analyticOrderAt f z₀

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

theorem analyticOrderNatAt_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} {z₀ : 𝕜} (hf : AnalyticAt 𝕜 f z₀) (n : ℕ) : analyticOrderNatAt (f ^ n) z₀ = n • analyticOrderNatAt f z₀

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

Level Sets of the Order Function

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

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

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

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.analyticOrderAt_ne_top_of_isPreconnected {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} {x y : 𝕜} (hf : AnalyticOnNhd 𝕜 f U) (hU : IsPreconnected U) (h₁x : x ∈ U) (hy : y ∈ U) (h₂x : analyticOrderAt f x ≠ ⊤) : analyticOrderAt f y ≠ ⊤

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_analyticOrderAt_eq_zero_or_top {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} (hf : AnalyticOnNhd 𝕜 f U) : {u : ↑U | analyticOrderAt f ↑u = 0 ∨ analyticOrderAt f ↑u = ⊤} ∈ Filter.codiscrete ↑U

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

theorem AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} (hf : AnalyticOnNhd 𝕜 f U) : {u : 𝕜 | analyticOrderAt f u = 0 ∨ analyticOrderAt f u = ⊤} ∈ Filter.codiscreteWithin U

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

theorem AnalyticOnNhd.preimage_zero_mem_codiscreteWithin {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E} {x : 𝕜} (h₁f : AnalyticOnNhd 𝕜 f U) (h₂f : f x ≠ 0) (hx : x ∈ U) (hU : IsConnected U) : f ⁻¹' {0}ᶜ ∈ Filter.codiscreteWithin U

If an analytic function f is not constantly zero on a connected set U, then its set of zeros is codiscrete within U.

See AnalyticOnNhd.preimage_mem_codiscreteWithin for a more general statement in preimages of codiscrete sets.

theorem AnalyticOnNhd.preimage_zero_mem_codiscrete {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} [ConnectedSpace 𝕜] {x : 𝕜} (hf : AnalyticOnNhd 𝕜 f Set.univ) (hx : f x ≠ 0) : f ⁻¹' {0}ᶜ ∈ Filter.codiscrete 𝕜

If an analytic function f is not constantly zero on 𝕜, then its set of zeros is codiscrete.

See AnalyticOnNhd.preimage_mem_codiscreteWithin for a more general statement in preimages of codiscrete sets.