| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Pure/ML/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 1 kB |
|
Quelle harmonic_polynomials.pvs Sprache: PVS |
|||||||||
|
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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28