| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/complex/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle fundamental_algebra.pvs Sprache: PVS |
|||||||||
|
fundamental_algebra: THEORY
%%% The Fundamental Theorem of Algebra %%% %%% Narkawicz 12/2013 %%% BEGIN IMPORTING exp n : VAR nat pn: VAR posnat a,b : VAR [nat->complex] c,x,y : VAR complex r,s : VAR real ff,gg:VAR [complex->complex] K : VAR posreal %Powers *(a,b)(n): complex = a(n)*b(n); +(a,b)(n): complex = a(n)+b(n); *(c,a)(n): complex = c*a(n); cfunmult(ff,gg)(c): complex = ff(c)*gg(c); cfunplus(ff,gg)(c): complex = ff(c) + gg(c); mult_0_l: LEMMA 0*c = 0 mult_commutes: LEMMA x*y = y*x cpow(c)(n): RECURSIVE complex = IF n = 0 THEN 1 ELSE c*cpow(c)(n-1) ENDIF MEASURE n cpow_0: LEMMA cpow(c)(pn)=0 IFF c=0 cpow_real: LEMMA cpow(r)(n) = r^n abs_rewrite: LEMMA abs(s*i + r) = sqrt(s^2 + r^2) arg_cpow: LEMMA -pi < pn*arg(c) AND pn*arg(c)<=pi IMPLIES arg(cpow(c)(pn)) = pn*arg(c) abs_cpow: LEMMA abs(cpow(c)(n)) = abs(c)^n abs_cpow_increasing: LEMMA abs(x)<=abs(y) IMPLIES abs(cpow(x)(n))<=abs(cpow(y)(n)) cpow_exp: LEMMA cpow(exp(c))(n) = exp(n*c) cpow_mult: LEMMA cpow(x*y)(n) = cpow(x)(n)*cpow(y)(n) %%% Continuity %%% complex_continuous?(ff): bool = FORALL (x:complex,epsil:posreal): EXISTS (delta:posreal): FORALL (y:complex): abs(x-y)<=delta IMPLIES abs(ff(x)-ff(y))<epsil complex_continuous_sum: LEMMA complex_continuous?(ff) AND complex_continuous?(gg) IMPLIES complex_continuous?(cfunplus(ff,gg)) complex_continuous_mult: LEMMA complex_continuous?(ff) AND complex_continuous?(gg) IMPLIES complex_continuous?(cfunmult(ff,gg)) complex_continuous_cpow: LEMMA complex_continuous?(LAMBDA (x): c*cpow(x)(n)) %%% Roots of Unity %%% root_neg_1(pn): complex = IF pn = 1 THEN -1 ELSE exp((i*pi)/pn) ENDIF root_neg_1_def: LEMMA cpow(root_neg_1(pn))(pn) = -1 root_complex(c)(pn): complex = from_polar(root_real(abs(c))(pn),arg(c)/pn) arg_root_complex: LEMMA arg(root_complex(c)(pn)) = arg(c)/pn abs_root_complex : LEMMA abs(root_complex(c)(pn)) = root_real(abs(c))(pn) root_complex_def: LEMMA cpow(root_complex(c)(pn))(pn) = c %%% Sums %%% csigma(a,n): RECURSIVE complex = IF n = 0 THEN a(0) ELSE a(n)+csigma(a,n-1) ENDIF MEASURE n csigma_plus: LEMMA csigma(a+b,n) = csigma(a,n)+csigma(b,n) csigma_scal_right: LEMMA csigma(a,n)*c = csigma(c*a,n) csigma_eq: LEMMA (FORALL (i:nat): i<=n IMPLIES a(i)=b(i)) IMPLIES csigma(a,n) = csigma(b,n) csigma_real_triangle: LEMMA abs(csigma(a,n))<=sigma(0,n,LAMBDA (i:nat): abs(a(i))) %%% Polynomials %%% cpolynomial(a,n)(c): complex = csigma(a*cpow(c),n) cpolynomial_rec: LEMMA cpolynomial(a,1+n)(c) = cpolynomial(a,n)(c) + a(1+n)*cpow(c)(1+n) cpolynomial_struct_rec: LEMMA cpolynomial(a,1+n)(c) = cpolynomial(LAMBDA (i:nat): a(i+1),n)(c)*c + a(0) cpolynomial_add: LEMMA cpolynomial(a+b,n) = cfunplus(cpolynomial(a,n),cpolynomial(b,n)) cpolynomial_eq_le_degree: LEMMA (FORALL (i:nat): i<=n IMPLIES a(i) = b(i)) IMPLIES cpolynomial(a,n) = cpolynomial(b,n) complex_continuous_cpolynomial: LEMMA complex_continuous?(cpolynomial(a,n)) complex_binomial_theorem: LEMMA cpow(x+y)(n) = csigma(LAMBDA (i:nat): IF i<=n THEN C(n,i)*cpow(x)(i)*cpow(y)(n-i) ELSE 0 ENDIF,n) complex_poly_shift: LEMMA EXISTS (b): b(0) = cpolynomial(a,n)(c) AND FORALL (x): cpolynomial(a,n)(x) = cpolynomial(b,n)(x-c) cpolynomial_limit_infinity: LEMMA n > 0 AND a(n)/=0 IMPLIES EXISTS (M:posnat): FORALL (x): abs(x)>=M IMPLIES abs(cpolynomial(a,n)(x)) > K complex_disk_complete: LEMMA (FORALL (j:nat): abs(a(j))<=K) IMPLIES EXISTS (c): abs(c)<=K AND FORALL (epsil:posreal,N:nat): EXISTS (j:nat): j>N AND abs(c-a(j))<epsil cpolynomial_attains_minimum: LEMMA EXISTS (c): FORALL (x): abs(cpolynomial(a,n)(c))<=abs(cpolynomial(a,n)(x)) fundamental_algebra: LEMMA n>0 AND a(n)/=0 IMPLIES EXISTS (c): cpolynomial(a,n)(c) = 0 END fundamental_algebra ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28