# RecurrenceRelations.ml

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

INCLUDE "preamble.ml"

let title (notation, _, _, point, _, _, _, _, _) =
<:text<\
Recurrence Relations for the Power Series Coefficients of \
<:imath< \$(str: notation) >> at <:isymb< \$(point) >>\
>>

let_service RecurrenceRelations
(notation : string)
(linear_comb_enc : any maple)
(def : diffeq maple)
(point : any maple)
(y : name maple)
(x : name maple)
(u : name maple)
(n : name maple)
(analytic : bool) :
DC.sec_entities * unit with { title = title } =

let linear_comb = << DDMF:-decode_linear_combination(\$(linear_comb_enc)) >> in

(* Extract the mathematical expression of the expansion, as well as the *)
(* system of recurrence equations and initial conditions. *)
let expr =
<<
`+`(op(zip((a, b) -> `if`(op(0, b) = `+`, map(c -> a * c, b), a * b),
map2(op, 1, \$(linear_comb)),
map(a -> DDMF:-transseries_to_expression(a[2]), \$(linear_comb)))));
>>
and recsys =
<<
map(a -> `if`(a[2]:-closed_form = 0, NULL, op(a[2]:-recurrences)),
\$(linear_comb))
>>
and inits =
<<
map(a -> `if`(a[2]:-closed_form = 0, NULL, op(a[2]:-initial_conditions)),
\$(linear_comb))
>> in

(* Rename the occurring sequences such as to avoid double indices and *)
(* to enforce a consecutive labeling of the sequences. *)
let rename =
<< DDMF:-rename_sequences([\$(expr), \$(recsys), \$(inits)], \$(u))[1] >> in
let expr = << \$(rename)[1] >>
and recsys = << \$(rename)[2] >>
and inits = << \$(rename)[3] >> in

(* Create the text to be displayed. *)
let expansion_text =
<:par<
Expansion of <:imath< \$(str: notation) >> at <:isymb< \$(point) >>:
<:dmath< \$(str: notation) = \$(symb: expr).>>
>> in
let recs_inits_text =
if <:bool< \$(recsys) <> [] >> then
let sOrNo1 = Wording.ending_of_seq recsys
and sOrNo2 = Wording.ending_of_seq inits in
<:par<
The first coefficients are given by the initial
condition\$(str:sOrNo2): <:dmath<<< op(\$(inits)) >>.>>
>> @:@
<:par<
The remaining coefficients can be computed by the
following recurrence equation\$(str:sOrNo1):
>> @:@
(List.fold_left (@:@) <:par<>>
(List.map
(fun i -> <:par<<:dmath<<< op(\$(int:i), \$(recsys)) >>, >>>>)
(CommonTools.range (<:int< nops(\$(recsys)) >> - 1)))) @:@
<:par<<:dmath<<< op(-1, \$(recsys)) >>.>>>>
else DC.ent_null in
let proof_text =
try
if not analytic then raise Exit;
ignore << gfun:-diffeqtorec(\$(def), \$(y)(\$(x)), \$(u)(\$(n))) >> ;