SSL harmonic_polynomials.pvs   Interaktion und
PortierbarkeitPVS

harmonic_polynomials: THEORY
BEGIN

  IMPORTING sq, sigma_nat, binomial

  pn:  VAR posnat
  x,y: VAR real

  harmonic_poly_real(pn:posnat,x,y:real):real
    = sigma(0,pn,LAMBDA (i:nat):
                 IF i > pn OR odd?(i) THEN 0 ELSE (-1)^(i/2)*C(pn,i)*
                      (IF    i = 0  THEN x^pn
                       ELSIF i = pn THEN y^pn
                                    ELSE x^(pn-i)*y^i ENDIF) ENDIF)

  harmonic_poly_imag(pn:posnat,x,y:real):real
    = sigma(0,pn,LAMBDA (i:nat):
                 IF i > pn OR even?(i) THEN 0 ELSE (-1)^((i-1)/2)*C(pn,i)*
                      (IF    i = pn THEN y^pn
                                    ELSE x^(pn-i)*y^i ENDIF) ENDIF)

  harmonic_polynomial_real_n1:  LEMMA harmonic_poly_real(1,x,y) = x
 
  harmonic_polynomial_imag_n1:  LEMMA harmonic_poly_imag(1,x,y) = y

  harmonic_polynomial_real_rec: LEMMA
      harmonic_poly_real(pn+1,x,y)
        = x*harmonic_poly_real(pn,x,y) - y*harmonic_poly_imag(pn,x,y)

  harmonic_polynomial_imag_rec: LEMMA
      harmonic_poly_imag(pn+1,x,y)
        = x*harmonic_poly_imag(pn,x,y) + y*harmonic_poly_real(pn,x,y)

  harmonic_polynomial_modulus: LEMMA
      sq(harmonic_poly_real(pn,x,y)) + sq(harmonic_poly_imag(pn,x,y))
    = (sq(x)+sq(y))^pn
    
END harmonic_polynomials