# SymmetriesProof.ml

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

INCLUDE "preamble.ml"

(* Displays a proof that a function is even/odd. *)
(* Input: *)
(*   def: in the format of defESF *)
(*   yofz: function symbol *)
(*   func_of_var: string with latex representation of the function *)
(*   func_of_neg: string of the function with negative argument *)
(*   symmetry: string ("even","odd", or anything else). *)
(*             Only used for the heading. If neither "even" nor "odd", *)
(*             then a generic heading is used. *)
(* If the function is neither even nor odd, then currently no
appropriate text is generated. *)

(* TODO return string "even", "odd", "no_symmetry_detected" *)
let title (_, _, func_of_var, _, symmetry) =
match symmetry with
| "even" ->
<:text<Proof That the Function <:imath<\$(str: func_of_var)>> is Even>>
| "odd" ->
<:text<Proof That the Function <:imath<\$(str: func_of_var)>> is Odd>>
| _ ->
<:text<Symmetry Proof for the Function <:imath<\$(str: func_of_var)>>>>

let_service SymmetriesProof
(def : diffeq maple)
(yofz : fcall maple)
(func_of_var : string)
(func_of_neg : string)
(str_sym : string) :
DC.sec_entities * string with { title = title } =
<:unit< unassign('iniconds', 'y', 'x') >> ;

let body = DC.ent_null in
<:unit<
fdiffeq := gfun:-formatdiffeq([\$(def), \$(yofz)], 'y', 'x', 'iniconds')
>> ;
let body =
let ending = Wording.ending_of_seq << iniconds >> in
body @@@ <:par<
The function under consideration satisfies the differential equation
<:dsymb< op(remove(type, \$(def), equation)) = 0 >>
with initial condition\$(str:ending)
<:dmath< << op(iniconds) >> . >>
>> in

(* The following string is used below to distinguish the hom. equation *)
(* from the inhom. one. *)
let body, homStr =
if <:bool< op(1,fdiffeq) <> 0 >> then
let b, defHom =
HomogeneousDiffEqn.diffeqtohomdiffeq def (<< y(x) >> : fcall maple) in
begin
<:unit<
unassign('iniconds','y','x') ;
fdiffeq := gfun:-formatdiffeq(
[\$(defHom), \$(yofz)], 'y', 'x', 'iniconds')
>> ;
(body @@@
(<:par<
We first convert this inhomogeneous equation into a homogeneous one.
>> @@@ b),
"homogeneous")
end else (body, "") in

(* replace x,D by -x,-D in the differential equation *)
<:unit<
altDiffeq := subs(x = -x, fdiffeq):
for i from 2 to nops(altDiffeq) do
if type(i, odd) then
altDiffeq := subsop(i = -op(i,altDiffeq), altDiffeq)
end if
end do:
diffeqSymmetric := evalb(fdiffeq = altDiffeq)
>> ;

<:unit<
originRegular := evalb(subs(x=0, op(-1,fdiffeq)) <> 0):
enoughICs := evalb(nops(iniconds) = nops(fdiffeq) - 2):
isOdd := originRegular and enoughICs and diffeqSymmetric:
isEven := originRegular and enoughICs and diffeqSymmetric:
for i from 1 to nops(iniconds) do
if (-1)^i*op(2,op(i,iniconds)) <> -op(2,op(i,iniconds)) then
isEven := false;
end if;
if (-1)^i*op(2,op(i,iniconds)) <> op(2,op(i,iniconds)) then
isOdd := false;
end if;
end do
>> ;

let is_even, is_odd = (<:bool< isEven >>, <:bool< isOdd >>) in
let sign = if is_odd then "-" else "" in

<:unit< funcSign := \$(int:if is_odd then -1 else 1) >> ;

let ret =
if is_even then "even"
else if is_odd then "odd"
else "no_symmetry_detected" in

<:unit<
inicondsAlt := iniconds ;
for i from 1 to nops(iniconds) do
inicondsAlt :=
subsop(i = subsop(2 = (-1)^i * funcSign * op(2, op(i,iniconds)),
op(i,iniconds)), inicondsAlt)
end do ;
unassign('i') ;
inicondsAlt := subs(y = y[1], iniconds)
>> ;
let ending = Wording.ending_of_seq << inicondsAlt >> in
let body = body @@@
<:par<
The \$(str:homStr) differential equation and the fact that
<:dmath<
<< diff(y(-x),[x\$i]) = (-1)^i*diff(y(x),[x\$i]) >>,
>>
imply that the function <:imath< y_1(x) = \$(str:sign)y(-x) >> satisfies
the differential equation
<:dsymb<
i=seq(nops(altDiffeq)-2..0,-1)) = -op(1,altDiffeq)
>>
with initial condition\$(str:ending)
<:dmath< << op(inicondsAlt) >> . >>
>> in

let body = body @@@
<:par<
The functions <:imath< \$(str: func_of_var) >>
and <:imath< \$(str:sign)\$(str: func_of_neg) >>
thus satisfy the same differential equation, and their derivatives at
<:imath< x = 0 >> agree up to order <:isymb< nops(iniconds)-1 >>.
Since <:imath< x = 0 >> is an \$(t_ent:Glossary.g "ordinary_point") of
the equation, these functions are analytic and equal in a neighborhood
of 0:
<:dmath< \$(str: func_of_var) = \$(str:sign)\$(str: func_of_neg) . >>
This identity extends to the whole common domain of definition of these
functions by uniqueness of the analytic continuation.
>> in
DC.section (title _req_params) body, ret

(* TODO test also for a singularity-free strip, not only for a disk *)

(* TODO check that the iniconds are indeed the first derivatives at zero *)
(* TODO return ret ; *)
```

Generated by GNU Enscript 1.6.5.90.