Factorized Rational Functions #
This file discusses functions π β π
of the form βαΆ u, (Β· - u) ^ d u
, where d : π β β€
is
integer-valued. We show that these "factorized rational functions" are meromorphic in normal form,
with divisor equal to d
.
Under suitable assumptions, we show that meromorphic functions are equivalent, modulo equality on codiscrete sets, to the product of a factorized rational function and an analytic function without zeros.
Implementation Note: For consistency, we use βαΆ u, (Β· - u) ^ d u
throughout. If the support of d
is finite, then evaluation of functions commutes with finprod, and the helper lemma
Function.FactorizedRational.finprod_eval
asserts that βαΆ u, (Β· - u) ^ d u
equals the function
fun x β¦ βαΆ u, (x - u) ^ d u
. If d
has infinite support, this equality is wrong in general.
There are elementary examples of functions d
where βαΆ u, (Β· - u) ^ d u
is constant one, while
fun x β¦ βαΆ u, (x - u) ^ d u
is not continuous.
Elementary Properties of Factorized Rational Functions #
Helper Lemma: Identify the support of d
as the mulsupport of the product defining the factorized
rational function.
Helper Lemma: If the support of d
is finite, then evaluation of functions commutes with finprod,
and the function βαΆ u, (Β· - u) ^ d u
equals fun x β¦ βαΆ u, (x - u) ^ d u
.
Factorized rational functions are analytic wherever the exponent is non-negative.
Helper Lemma for Computations: Extract one factor out of a factorized rational function.
Factorized rational functions are meromorphic in normal form on univ
.
Factorized rational functions are meromorphic in normal form on arbitrary subsets of π
.
Orders and Divisors of Factorized Rational Functions #
The order of the factorized rational function (βαΆ u, fun z β¦ (z - u) ^ d u)
at z
equals d z
.
Alias of Function.FactorizedRational.meromorphicOrderAt_eq
.
The order of the factorized rational function (βαΆ u, fun z β¦ (z - u) ^ d u)
at z
equals d z
.
Factorized rational functions are nowhere locally constant zero.
Alias of Function.FactorizedRational.meromorphicOrderAt_ne_top
.
Factorized rational functions are nowhere locally constant zero.
If D
is a divisor, then the divisor of the factorized rational function equals D
.
Elimination of Zeros and Poles #
This section shows that every meromorphic function with finitely many zeros and poles is equivalent, modulo equality on codiscrete sets, to the product of a factorized rational function and an analytic function without zeros.
We provide analogous results for functions of the form log βmeromorphicβ
.
TODO: Identify some of the terms that appear in the decomposition.
If f
is meromorphic on an open set U
, if f
is nowhere locally constant zero, and if the
support of the divisor of f
is finite, then there exists an analytic function g
on U
without
zeros such that f
is equivalent, modulo equality on codiscrete sets, to the product of g
and the
factorized rational function associated with the divisor of f
.
In the setting of MeromorphicOn.extract_zeros_poles
, the function log βfβ
is equivalent, modulo
equality on codiscrete subsets, to βαΆ u, (divisor f U u * log βΒ· - uβ) + log βg Β·β
.