Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: 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

[ zur Elbe Produktseite wechseln0.17Quellennavigators  Analyse erneut starten  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik