# RatMajSeries.ml

```(* Copyright INRIA and Microsoft Corporation, 2008-2013. *)

INCLUDE "preamble.ml"

let title _ = <:text< Majorant series for rational functions >>

exception Warning of DC.sec_entities

let_service RatMajSeries
(r : any maple)
(x : name maple)
(g : any maple)
(a : any maple)
(m : int) :
DC.sec_entities * any maple option with { title = title } =
try

(* computation of the majorant series *)

let num = << numer(\$(r)) >> in
let den = << denom(\$(r)) >> in

let ispoly = <:bool< evalb(\$(den) = 1) >> in

if not ispoly then

let degden = <:int< degree(\$(den)) >> in

let numbound = << polyapprox:-polybound(\$(num), \$(x), \$(g), \$(a),
\$(int: m) / 2) >> in
let denbound = << polyapprox:-invpolybound(\$(den), \$(x), \$(g), \$(a),
\$(int: m) / 2) >> in

let numbound = << polyapprox:-pretty_print(\$(numbound)) >> in
let denbound = << polyapprox:-pretty_print(\$(denbound)) >> in
let cm = << polyapprox:-pretty_print(\$(numbound) * \$(denbound)) >> in

(* display it *)

let majseries = <:par< Let <:isymb< alpha = \$(g) * \$(a) >>, <:isymb< m =
\$(int: m) >>, <:isymb< M = \$(cm) >>. Then the function <:imath< \frac M
{(1 - \alpha \$(symb:x))^m} >> is a majorant series of
<:isymb< r(\$(x)) = \$(r) >>. >> in

(* proof *)

(* 1. Majorant series for the inverse of the denominator *)

let denomproof = DC.section <:text< Majorant series for the inverse of the
denominator >>

(<:par< First we find a majorant series for the inverse of the
denominator of <:isymb< r(\$(x)) >>. Let <:isymb< f(\$(x)) = 1 / \$(den) >> and
<:imath< \$(symb: den) = \prod_{i=1}^{\$(int: degden)} (1 - \alpha_i \$(symb:x))
>>. According to Newton's identities, we have:
<:dmath< \$(symb:x) f'(\$(symb:x)) = S(\$(symb:x)) f(\$(symb:x)), >> where
<:imath< S(\$(symb:x)) = \sum_{k=1}^\infty S_k \$(symb:x)^k >> and
<:imath< S_k = \sum_{i=1}^{\$(int: degden)} \alpha_i^k >>.
Let <:imath< \tilde\alpha = \max_i|\alpha_i| >>.
Then we have the following inequality: <:dmath< |S_k| \le \$(int: degden)
\tilde\alpha^k, >> for every <:imath< k >>. Moreover, using Graeffe's method,
<:imath< \alpha >> has been computed so that <:imath< \tilde\alpha < \alpha >>.
>> @@@

<:par< Now if we write <:imath< f(\$(symb:x)) =
\sum_{k=0}^\infty u_k \$(symb:x)^k >>, this equation becomes:
<:dmath< u_n = \frac 1 n \sum_{k=0}^{n-1} S_{n-k} u_k. >>
>> @@@

<:par< Suppose that for every <:imath< k < n >>, the following
inequality holds: <:dmath< |u_k| \le M_0 {k + m/2 - 1 \choose m/2 - 1} \alpha^k,
>> for some positive constant <:imath< M_0 >>. Then: <:dmath< |u_n| \le \frac 1
n \sum_{k = 0}^{n - 1} \$(int: degden) \tilde\alpha^{n-k} M_0 {k + m/2 - 1
\choose m / 2 - 1} \alpha ^ k >> And thus: <:dmath< |u_n| \le M_0 {n + m / 2 - 1
\choose m / 2 - 1} \alpha ^ n \frac {\$(int: degden)} n \sum_{k = 0}^{n - 1}
\left(\frac{\tilde\alpha} \alpha\right)^{n-k} \le M_0 {n + m/2 - 1 \choose m / 2
- 1} \alpha ^ n \frac {\$(int: degden)} n \frac 1 {1 - \frac{\tilde\alpha}
\alpha} >>
Hence, if we take: <:dmath< n_0 = \left\lceil \frac {\$(int: degden)} {1 -
\frac{\tilde\alpha} \alpha} \right\rceil, >> and: <:dmath< M_0 = \max_{n < n_0}
\frac {|u_k|} {{k + m/2 - 1 \choose m/2 - 1} \alpha ^ k}, >> then we get by
induction: <:dmath< |u_n| \le M_0 {n + m/2 - 1 \choose m/2 - 1} \alpha^n. >>
Thus, <:imath< \frac {M_0} {(1 - \alpha \$(symb:x)) ^ {m/2}} >>
is a majorant series of <:imath< f(\$(symb:x)) >>.
Numerically, we find <:isymb< M[0] = \$(denbound) >>. >>) in

(* 2. Majorant series for the rational function *)

let ratproof = DC.section <:text< Majorant series for the rational
function >>

(<:par< The aim is now to find a positive constant <:imath< M_1 >> such
that <:imath< \frac {M_1} {(1-\alpha \$(symb:x))^{m/2}} >>
is a majorant series of <:isymb< \$(num) >>. It suffices to take:
<:dmath< M_1 = \max_k \frac {|c_k|}
{ { k + m/2 - 1 \choose m/2 - 1 } \alpha ^ k}, >> where the <:imath< (c_k) >>
are the coefficients of <:isymb< \$(num) >>. Numerically, we get: <:imath< M_1 =
\$(symb: denbound) >> >> @@@

<:par< <:imath< \frac {M_0 M_1} {(1 - \alpha \$(symb:x)) ^ m} >> is
then a majorant series of <:imath< r(\$(symb:x)) >>. >>) in

(* final merge *)

let proof = DC.section <:text< Proof >> (denomproof @@@ ratproof) in

DC.section (title ())
((DC.section <:text< Statement >> majseries) @@@ proof),
Some <:symb< \$(numbound) * \$(denbound) >>

else

(* special case - not really a rational function but a (non-zero)
* polynomial. no need to split the exponent *)

let cm = << polyapprox:-polybound(\$(num), \$(x), \$(g), \$(a), \$(int: m)) >>
in
let cm = << polyapprox:-pretty_print(\$(cm)) >> in

let majseries = <:par< Let <:isymb< alpha = \$(g) * \$(a) >>, <:isymb< m =
\$(int: m) >>, <:isymb< M = \$(cm) >>. Then the function <:imath< \frac M
{(1 - \alpha \$(symb:x))^m} >> is a majorant series of
<:isymb< r(\$(x)) = \$(num) >>. >> in

(* "proof" *)

let proof = DC.section <:text< Proof >> <:par< The aim is to find a
positive constant <:imath< M >> such that <:imath< \frac {M}
{(1 - \alpha \$(symb:x))^m} >> is a majorant series of <:isymb< \$(num) >>.
It suffices to take: <:dmath< M = \max_k \frac {|c_k|}
{{ k + m - 1 \choose m - 1 } \alpha ^ k} \le \$(symb:cm), >>
where the <:imath< (c_k) >> are the coefficients of <:isymb<\$(num) >>. >> in

DC.section (title ())
((DC.section <:text< Statement >> majseries) @@@ proof),
Some cm

with (Warning msg) -> (DC.warning msg, None)

```

Generated by GNU Enscript 1.6.5.90.