RatMajSeries.ml

(* Copyright INRIA and Microsoft Corporation, 2008-2013. *)
(* DDMF is distributed under CeCILL-B license. *)

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.