Documentation

Mathlib.Analysis.Analytic.Order

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
@[deprecated analyticOrderAt (since := "2025-05-02")]
def AnalyticAt.order {๐•œ : Type u_1} {E : Type u_2} [NontriviallyNormedField ๐•œ] [NormedAddCommGroup E] [NormedSpace ๐•œ E] (f : ๐•œ โ†’ E) (zโ‚€ : ๐•œ) :

Alias of analyticOrderAt.


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
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 analyticand 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
@[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โ‚€.

@[deprecated analyticOrderAt_eq_top (since := "2025-05-03")]
theorem AnalyticAt.order_eq_top_iff {๐•œ : 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

Alias of analyticOrderAt_eq_top.


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โ‚€.

@[deprecated AnalyticAt.analyticOrderAt_eq_natCast (since := "2025-05-03")]
theorem AnalyticAt.order_eq_nat_iff {๐•œ : 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

Alias of AnalyticAt.analyticOrderAt_eq_natCast.


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.

@[deprecated AnalyticAt.analyticOrderAt_ne_top (since := "2025-05-03")]
theorem AnalyticAt.order_ne_top_iff {๐•œ : 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

Alias of AnalyticAt.analyticOrderAt_ne_top.


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.

@[deprecated AnalyticAt.analyticOrderAt_ne_top (since := "2025-02-03")]
theorem AnalyticAt.order_neq_top_iff {๐•œ : 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

Alias of AnalyticAt.analyticOrderAt_ne_top.


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โ‚€.

@[deprecated AnalyticAt.analyticOrderAt_eq_zero (since := "2025-05-03")]
theorem AnalyticAt.order_eq_zero_iff {๐•œ : 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

Alias of AnalyticAt.analyticOrderAt_eq_zero.


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 โ„•.

@[deprecated apply_eq_zero_of_analyticOrderNatAt_ne_zero (since := "2025-05-03")]
theorem AnalyticAt.apply_eq_zero_of_order_toNat_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

Alias of apply_eq_zero_of_analyticOrderNatAt_ne_zero.


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 โˆž.

@[deprecated natCast_le_analyticOrderAt (since := "2025-05-03")]
theorem natCast_le_order_iff {๐•œ : 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

Alias of natCast_le_analyticOrderAt.


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.

@[deprecated analyticOrderAt_congr (since := "2025-05-03")]
theorem AnalyticAt.order_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โ‚€

Alias of analyticOrderAt_congr.


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.

@[deprecated le_analyticOrderAt_add (since := "2025-05-03")]
theorem AnalyticAt.order_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โ‚€

Alias of le_analyticOrderAt_add.


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โ‚€
@[deprecated le_analyticOrderAt_add (since := "2025-05-03")]
theorem order_add_of_order_lt_order {๐•œ : 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โ‚€

Alias of le_analyticOrderAt_add.


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

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.

@[deprecated analyticOrderAt_add_of_ne (since := "2025-05-03")]
theorem AnalyticAt.order_add_of_order_ne_order {๐•œ : 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โ‚€)

Alias of analyticOrderAt_add_of_ne.


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โ‚€ = โŠค) :
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โ‚€ = โŠค) :
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

@[deprecated analyticOrderAt_centeredMonomial (since := "2025-05-03")]
theorem analyticAt_order_centeredMonomial {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {zโ‚€ : ๐•œ} {n : โ„•} :
analyticOrderAt ((fun (x : ๐•œ) => x - zโ‚€) ^ n) zโ‚€ = โ†‘n

Alias of analyticOrderAt_centeredMonomial.


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โ‚€ = โŠค
@[deprecated analyticOrderAt_mul_eq_top_of_left (since := "2025-05-03")]
theorem AnalyticAt.order_mul_of_order_eq_top {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f g : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : analyticOrderAt f zโ‚€ = โŠค) :
analyticOrderAt (f * g) zโ‚€ = โŠค

Alias of analyticOrderAt_mul_eq_top_of_left.

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.

@[deprecated analyticOrderAt_mul (since := "2025-05-03")]
theorem AnalyticAt.order_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โ‚€

Alias of analyticOrderAt_mul.


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.

@[deprecated analyticOrderAt_pow (since := "2025-05-03")]
theorem AnalyticAt.order_pow {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {f : ๐•œ โ†’ ๐•œ} {zโ‚€ : ๐•œ} (hf : AnalyticAt ๐•œ f zโ‚€) (n : โ„•) :
analyticOrderAt (f ^ n) zโ‚€ = n โ€ข analyticOrderAt f zโ‚€

Alias of analyticOrderAt_pow.


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} (hf : AnalyticOnNhd ๐•œ f U) {x y : ๐•œ} (hU : IsPreconnected U) (hโ‚x : x โˆˆ U) (hy : y โˆˆ U) (hโ‚‚x : analyticOrderAt f x โ‰  โŠค) :

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.