# TaylorTruncation.ml

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

INCLUDE "preamble.ml"

let title _ = <:text<Taylor Truncation>>

exception Warning of DC.sec_entities

let symbolic_r str =
if Str.string_match (Str.regexp "\\.[0-9]+\\|[0-9]+\\.?[0-9]*") str 0 then
<< convert(parse(\$(str:str)), 'rational', 'exact'): >>
else
raise (Warning <:par< <:imath< r >> should be a positive number. >>)

let_service TaylorTruncation
(deq : diffeq maple)
(y : name maple)
(x : name maple)
(notation : string)
(r : string = "0.3")
(prec : int = Constants.default_precision) :
DC.sec_entities * (int option) with { title = title } =
try

let deq = <<gfun:-diffeqtohomdiffeq(\$(deq), \$(y)(\$(x)))>> in

(* Detection of the singularities (FIXME?) *)

let rad = symbolic_r r in
let infsing =
<< gfun:-NumGfun:-utilities:-diffeq_infsing(\$(deq), \$(y)(\$(x))) >>
in
if <:bool< signum(\$(rad) - abs(\$(infsing))) >= 0 >> then
<:par< It is not easy to determine whether <:imath< \$(str: notation) >>
can be evaluated on the disk
<:imath< \mathopen| \$(symb: x) \mathclose| \leq \$(symb:rad) >>
using this power series expansion, since the said disk contains
<:imath< \$(symb:infsing) >>, which is a singular point
of the differential equation above. >>,
None
else

(* Computation of the polynomial approximation *)
let t = <:int< polyapprox:-taylortail(\$(deq), \$(y)(\$(x)), \$(rad),
10 ^ (-\$(int:prec)) / 2) >> in
let order = <:int< polyapprox:-optimize(\$(deq), \$(y)(\$(x)), \$(int: t),
\$(rad), 10 ^ (-\$(int:prec))) >> in

(* Display it *)

let approx =
<:par< Error bound for Taylor approximation on the disk
<:imath< \mathopen| \$(symb: x) \mathclose| \leq r = \$(symb:rad) >>:
<:dmath< \left|\sum_{n=0}^{\$(int: order)} u(n) \$(symb: x)^n
- \$(str: notation) \right| < 10^{ \$(int:-prec) }.
>> >>
in

(* Link to the proof *)

let ldescr =
TaylorTruncProof.descr (deq, y, x, notation, r, prec) None in
let rlink = DC.link_service ldescr <:text<Details>> in
let link = <:par< \$(rlink). >> in