SymmetriesProof.ml

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

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]) >>,
        \quad \text{for } i\in\mathbb{N},
      >>
      imply that the function <:imath< y_1(x) = $(str:sign)y(-x) >> satisfies
      the differential equation
      <:dsymb<
        add(op(i+2,altDiffeq) * diff(y[1](x),[x$i]),
            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.