Orders of Meromorphic Functions #
This file defines the order of a meromorphic function f at a point zβ, as an element of
β€ βͺ {β}.
We characterize the order being < 0, or = 0, or > 0, as the convergence of the function
to infinity, resp. a nonzero constant, resp. zero.
TODO #
Uniformize API between analytic and meromorphic functions
Order at a Point: Definition and Characterization #
The order of a meromorphic function 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 MeromorphicAt.meromorphicOrderAt_eq_top_iff and
MeromorphicAt.meromorphicOrderAt_eq_int_iff for these equivalences.
If the function is not meromorphic at x, we use the junk value 0.
Equations
- meromorphicOrderAt f x = if hf : MeromorphicAt f x then ENat.map (fun (x : β) => βx) (analyticOrderAt (fun (z : π) => (z - x) ^ Exists.choose hf β’ f z) x) - β(Exists.choose hf) else 0
Instances For
Alias of meromorphicOrderAt.
The order of a meromorphic function 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 MeromorphicAt.meromorphicOrderAt_eq_top_iff and
MeromorphicAt.meromorphicOrderAt_eq_int_iff for these equivalences.
If the function is not meromorphic at x, we use the junk value 0.
Equations
Instances For
The order of a meromorphic function f at a zβ is infinity iff f vanishes locally around
zβ.
Alias of meromorphicOrderAt_eq_top_iff.
The order of a meromorphic function f at a zβ is infinity iff f vanishes locally around
zβ.
The order of a meromorphic function f at zβ equals an integer 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 meromorphicOrderAt_eq_int_iff.
The order of a meromorphic function f at zβ equals an integer 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 a meromorphic 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β.
Alias of meromorphicOrderAt_ne_top_iff.
The order of a meromorphic 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β.
The order of a meromorphic function f at zβ is finite iff f does not have
any zeros in a sufficiently small neighborhood of zβ.
Alias of meromorphicOrderAt_ne_top_iff_eventually_ne_zero.
The order of a meromorphic function f at zβ is finite iff f does not have
any zeros in a sufficiently small neighborhood of zβ.
If the order of a meromorphic function is negative, then this function converges to infinity
at this point. See also the iff version tendsto_cobounded_iff_meromorphicOrderAt_neg.
Alias of tendsto_cobounded_of_meromorphicOrderAt_neg.
If the order of a meromorphic function is negative, then this function converges to infinity
at this point. See also the iff version tendsto_cobounded_iff_meromorphicOrderAt_neg.
If the order of a meromorphic function is zero, then this function converges to a nonzero
limit at this point. See also the iff version tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero.
Alias of tendsto_ne_zero_of_meromorphicOrderAt_eq_zero.
If the order of a meromorphic function is zero, then this function converges to a nonzero
limit at this point. See also the iff version tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero.
If the order of a meromorphic function is positive, then this function converges to zero
at this point. See also the iff version tendsto_zero_iff_meromorphicOrderAt_pos.
Alias of tendsto_zero_of_meromorphicOrderAt_pos.
If the order of a meromorphic function is positive, then this function converges to zero
at this point. See also the iff version tendsto_zero_iff_meromorphicOrderAt_pos.
If the order of a meromorphic function is nonnegative, then this function converges
at this point. See also the iff version tendsto_nhds_iff_meromorphicOrderAt_nonneg.
Alias of tendsto_nhds_of_meromorphicOrderAt_nonneg.
If the order of a meromorphic function is nonnegative, then this function converges
at this point. See also the iff version tendsto_nhds_iff_meromorphicOrderAt_nonneg.
A meromorphic function converges to infinity iff its order is negative.
Alias of tendsto_cobounded_iff_meromorphicOrderAt_neg.
A meromorphic function converges to infinity iff its order is negative.
A meromorphic function converges to a limit iff its order is nonnegative.
Alias of tendsto_nhds_iff_meromorphicOrderAt_nonneg.
A meromorphic function converges to a limit iff its order is nonnegative.
A meromorphic function converges to a nonzero limit iff its order is zero.
Alias of tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero.
A meromorphic function converges to a nonzero limit iff its order is zero.
A meromorphic function converges to zero iff its order is positive.
Alias of tendsto_zero_iff_meromorphicOrderAt_pos.
A meromorphic function converges to zero iff its order is positive.
Meromorphic functions that agree in a punctured neighborhood of zβ have the same order at
zβ.
Alias of meromorphicOrderAt_congr.
Meromorphic functions that agree in a punctured neighborhood of zβ have the same order at
zβ.
Compatibility of notions of order for analytic and meromorphic functions.
Alias of AnalyticAt.meromorphicOrderAt_eq.
Compatibility of notions of order for analytic and meromorphic functions.
When seen as meromorphic functions, analytic functions have nonnegative order.
Alias of AnalyticAt.meromorphicOrderAt_nonneg.
When seen as meromorphic functions, analytic functions have nonnegative order.
If a function is both meromorphic and continuous at a point, then it is analytic there.
Order at a Point: Behaviour under Ring Operations #
We establish additivity of the order under multiplication and taking powers.
The order is additive when multiplying scalar-valued and vector-valued meromorphic functions.
Alias of meromorphicOrderAt_smul.
The order is additive when multiplying scalar-valued and vector-valued meromorphic functions.
The order is additive when multiplying meromorphic functions.
Alias of meromorphicOrderAt_mul.
The order is additive when multiplying meromorphic functions.
The order multiplies by n when taking a meromorphic function to its nth power.
Alias of meromorphicOrderAt_pow.
The order multiplies by n when taking a meromorphic function to its nth power.
The order multiplies by n when taking a meromorphic function to its nth power.
Alias of meromorphicOrderAt_zpow.
The order multiplies by n when taking a meromorphic function to its nth power.
The order of the inverse is the negative of the order.
Alias of meromorphicOrderAt_inv.
The order of the inverse is the negative of the order.
The order of a sum is at least the minimum of the orders of the summands.
Alias of meromorphicOrderAt_add.
The order of a sum is at least the minimum of the orders of the summands.
Helper lemma for meromorphicOrderAt_add_of_ne.
Alias of meromorphicOrderAt_add_eq_left_of_lt.
Helper lemma for meromorphicOrderAt_add_of_ne.
Helper lemma for meromorphicOrderAt_add_of_ne.
If two meromorphic functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.
Alias of meromorphicOrderAt_add_of_ne.
If two meromorphic functions have unequal orders, then the order of their sum is exactly the minimum of the orders of the summands.
Alias of meromorphicOrderAt_add_of_ne.
If two meromorphic 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 #
The set where a meromorphic function has infinite order is clopen in its domain of meromorphy.
Alias of MeromorphicOn.isClopen_setOf_meromorphicOrderAt_eq_top.
The set where a meromorphic function has infinite order is clopen in its domain of meromorphy.
On a connected set, there exists a point where a meromorphic function f has finite order iff
f has finite order at every point.
Alias of MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall.
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.
Alias of MeromorphicOn.meromorphicOrderAt_ne_top_of_isPreconnected.
On a preconnected set, a meromorphic function has finite order at one point if it has finite order at another point.
If a function is meromorphic on a set U, then for each point in U, it is analytic at nearby
points in U. When the target space is complete, this can be strengthened to analyticity at all
nearby points, see MeromorphicAt.eventually_analyticAt.
Meromorphic functions on U are analytic on U, outside of a discrete subset.
The set where a meromorphic function has zero or infinite order is codiscrete within its domain of meromorphicity.
Alias of MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top.
The set where a meromorphic function has zero or infinite order is codiscrete within its domain of meromorphicity.