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 #
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
Instances For
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
Instances For
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
- analyticOrderNatAt f zโ = (analyticOrderAt f zโ).toNat
Instances For
The order of a function f
at a zโ
is infinity iff f
vanishes locally around zโ
.
Alias of analyticOrderAt_eq_top
.
The order of a function f
at a zโ
is infinity iff f
vanishes locally around 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โ
.
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โ
.
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โ
.
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.
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.
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.
The order of an analytic function f
at zโ
is zero iff f
does not vanish at zโ
.
Alias of AnalyticAt.analyticOrderAt_eq_zero
.
The order of an analytic function f
at zโ
is zero iff f
does not vanish at zโ
.
The order of an analytic function f
at zโ
is zero iff f
does not vanish at zโ
.
A function vanishes at a point if its analytic order is nonzero in โโ
.
A function vanishes at a point if its analytic order is nonzero when converted to โ.
Alias of apply_eq_zero_of_analyticOrderNatAt_ne_zero
.
A function vanishes at a point if its analytic order is nonzero when converted to โ.
Characterization of which natural numbers are โค hf.order
. Useful for avoiding case splits,
since it applies whether or not the order is โ
.
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 โ
.
If two functions agree in a neighborhood of zโ
, then their orders at zโ
agree.
Alias of analyticOrderAt_congr
.
If two functions agree in a neighborhood of zโ
, then their orders at zโ
agree.
The order of a sum is at least the minimum of the orders of the summands.
Alias of le_analyticOrderAt_add
.
The order of a sum is at least the minimum of the orders of the summands.
Alias of le_analyticOrderAt_add
.
The order of a sum is at least the minimum of the orders of the summands.
If two functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.
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.
The order is additive when scalar multiplying analytic functions.
Vanishing Order at a Point: Elementary Computations #
Simplifier lemma for the order of a centered monomial
Alias of analyticOrderAt_centeredMonomial
.
Simplifier lemma for the order of a centered monomial
Alias of analyticOrderAt_mul_eq_top_of_left
.
The order is additive when multiplying analytic functions.
Alias of analyticOrderAt_mul
.
The order is additive when multiplying analytic functions.
The order is additive when multiplying analytic functions.
The order multiplies by n
when taking an analytic function to its n
th power.
Alias of analyticOrderAt_pow
.
The order multiplies by n
when taking an analytic function to its n
th power.
The order multiplies by n
when taking an analytic function to its n
th power.
Level Sets of the Order Function #
The set where an analytic function has infinite order is clopen in its domain of analyticity.
On a connected set, there exists a point where a meromorphic function f
has finite order iff
f
has finite order at every point.
On a preconnected set, a meromorphic function has finite order at one point if it has finite order at another point.
The set where an analytic function has zero or infinite order is discrete within its domain of analyticity.