Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: fundamental_algebra.pvs Sprache: PVS

Original von: 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.5 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.