|
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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
