more_polynomial_props.pvs Interaktion und
PortierbarkeitPVS

more_polynomial_props: THEORY
BEGIN

  IMPORTING polynomials,sign,log_nat,min_max

  a,b,h : VAR sequence[real]
  n   : VAR nat
  m,p   : VAR nat
  x,y,z : VAR real

  polynomial_degree_existence: LEMMA
    ((EXISTS (x): polynomial(a,n)(x)/=0) OR
     (EXISTS (i:upto(n)): a(i)/=0))
    IMPLIES
    EXISTS (i:upto(n)): a(i)/=0 AND
      (FORALL (j:nat): j>i AND j<=n IMPLIES a(j) = 0) AND
      polynomial(a,n) = polynomial(a,i)

  square_free?(a,n): bool =
    FORALL (y:real,g:sequence[real],k:nat): polynomial(a,n)(y)=0 AND
      (FORALL (x:real): polynomial(a,n)(x) = (x-y)*polynomial(g,k)(x))
      IMPLIES
      polynomial(g,k)(y)/=0

  poly_deriv_limit: LEMMA
    FORALL (y:real,epsil:posreal,pn:posnat): EXISTS (delta:posreal):
      FORALL (x:real): abs(x-y)<delta AND x/=y IMPLIES
        abs(polynomial(poly_deriv(a),pn-1)(y) -
     (polynomial(a,pn)(x)-polynomial(a,pn)(y))/(x-y)) < epsil

  square_free_min: LEMMA
    FORALL (epsil:posreal,y,c:real,pn:posnat): polynomial(a,pn)(y) = c AND
   (FORALL (x:real): abs(x-y)<epsil IMPLIES polynomial(a,pn)(x)>=c)
   IMPLIES
   polynomial(poly_deriv(a),pn-1)(y) = 0

  square_free_max: LEMMA
    FORALL (epsil:posreal,y,c:real,pn:posnat): polynomial(a,pn)(y) = c AND
   (FORALL (x:real): abs(x-y)<epsil IMPLIES polynomial(a,pn)(x)<=c)
   IMPLIES
   polynomial(poly_deriv(a),pn-1)(y) = 0

  IMPORTING binomial_identities

  deriv_poly_shift: LEMMA n>0 AND (FORALL (i:nat):i>n IMPLIES a(i)=0)
           IMPLIES
     poly_deriv(poly_shift(a,n)(y)) =
           poly_shift(poly_deriv(a),n-1)(y)

  linear_power_is_differentiable: LEMMA
    m>0 IMPLIES EXISTS (a): a(m)=1 AND
    (FORALL (i:nat): i>m IMPLIES a(i)=0) AND
    (FORALL (x): polynomial(a,m)(x) = (x-y)^m) AND
    (FORALL (x): polynomial(poly_deriv(a),m-1)(x)=m*(x-y)^(m-1))

  polynomial_prod_degrees: LEMMA
    FORALL (a,b,g:[nat->real],n,m,p:nat):
    (FORALL (x): polynomial(a,n)(x) = polynomial(b,m)(x)*polynomial(g,p)(x)) AND
    a(n)/=0 AND b(m)/=0 AND g(p)/=0 IMPLIES
    (n=m+p AND FORALL (i:nat): i<=n IMPLIES a(i) = polynomial_prod(b,m,g,p)(i))

  polynomial_div_linear_power_degree: LEMMA
    FORALL (a,b:[nat->real],n,m,k:nat):
      (FORALL (x): polynomial(a,n)(x) = (x-y)^k*polynomial(b,m)(x)) AND
      a(n)/=0 AND b(m)/=0
      IMPLIES
      (a(n)=b(m) AND n=m+k)

  poly_deriv_signs_neq_around_root_left: LEMMA n>0 AND
    x < y AND
    polynomial(a,n)(y) = 0 AND
    (FORALL (z:real): x<=z AND z<=y AND
                (polynomial(a,n)(z)=0 OR polynomial(poly_deriv(a),n-1)(z)=0)
        IMPLIES z=y)
    IMPLIES sign_ext(polynomial(a,n)(x)) = -sign_ext(polynomial(poly_deriv(a),n-1)(x))

  poly_deriv_signs_neq_around_root_right: LEMMA n>0 AND
    x > y AND
    polynomial(a,n)(y) = 0 AND
    (FORALL (z:real): y<=z AND z<=x AND
                (polynomial(a,n)(z)=0 OR polynomial(poly_deriv(a),n-1)(z)=0)
        IMPLIES z=y)
    IMPLIES sign_ext(polynomial(a,n)(x)) = sign_ext(polynomial(poly_deriv(a),n-1)(x))

  % Every polynomial is divisible by a maximal power (x-y)^m

  max_linear_div_power?(a,n,y)(m:posnat): bool =
    EXISTS (b,q:[nat->real]): m<=n AND
      (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
      polynomial(b,n-m)(y)/=0 AND
      (FORALL (x): polynomial(poly_deriv(a),n-1)(x) = (x-y)^(m-1)*polynomial(q,n-m)(x)) AND
      polynomial(q,n-m)(y)/=0

  max_linear_div_power_rew: LEMMA FORALL (m:posnat):
    max_linear_div_power?(a,n,y)(m) IFF
    (m<=n AND EXISTS (b:[nat->real]):
      (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
       polynomial(b,n-m)(y)/=0)

  max_linear_div_power_rew2: LEMMA FORALL (m:posnat):
    max_linear_div_power?(a,n,y)(m) IFF
    (EXISTS (b:[nat->real],k:nat):
      (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,k)(x)) AND
       polynomial(b,k)(y)/=0)

  max_linear_div_power_unique: LEMMA FORALL (m,kp:posnat):
    max_linear_div_power?(a,n,y)(m) AND
    max_linear_div_power?(a,n,y)(kp)
    IMPLIES
    m=kp

  max_linear_div_power_additive: LEMMA FORALL (m,kp:posnat,b:[nat->real],k:nat):
    max_linear_div_power?(b,k,y)(kp) AND
    (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,k)(x))
    IMPLIES
    max_linear_div_power?(a,n,y)(m+kp)

  max_linear_div_power_derivative: LEMMA
    FORALL (m:posnat): m>1 IMPLIES
      (max_linear_div_power?(a,n,y)(m) IMPLIES
      (n>0 AND max_linear_div_power?(poly_deriv(a),n-1,y)(m-1)))

  % compute_max_lin_div_pow(a,(n|a(n)/=0),y): RECURSIVE {k:nat|
  %   (k=0 IMPLIES polynomial(a,n)(y)/=0) AND
  %   (k>0 IMPLIES max_linear_div_power?(a,n,y)(k))} =
  %     IF polynomial(a,n)(y)/=0 THEN 0
  %     ELSIF n = 1 THEN 1
  %     ELSIF

  poly_max_zero_power: LEMMA polynomial(a,n)(y)=0 AND a(n)/=0 IMPLIES
    EXISTS (m:posnat): max_linear_div_power?(a,n,y)(m)

  max_linear_div_power_scal: LEMMA FORALL (nz:nzreal,m:posnat):
    max_linear_div_power?(a,n,y)(m) IFF
    max_linear_div_power?(nz*a,n,y)(m)

  max_linear_div_power_lower_bound: LEMMA FORALL (b:[nat->real],k,j:nat,m:posnat):
    max_linear_div_power?(a,n,y)(m) AND
    (FORALL (x): polynomial(a,n)(x)=(x-y)^k*polynomial(b,j)(x))
    IMPLIES
    k<=m AND (k=m IFF polynomial(b,j)(y)/=0)

  div_linear_power_reduces: LEMMA FORALL (b:[nat->real],k,j,d:nat):
    (FORALL (x): polynomial(a,n)(x) = (x-y)^k*polynomial(b,j)(x))
    AND k>=d IMPLIES
    (EXISTS (bb:[nat->real],q:nat):
      FORALL (x): polynomial(a,n)(x) = (x-y)^d*polynomial(bb,q)(x))

  max_linear_div_power_sign_change: LEMMA FORALL (m:posnat):
    x < y AND y < z AND
    (FORALL (r:real): x<= r AND r<= z AND polynomial(a,n)(r) = 0
         IMPLIES r = y) AND
    max_linear_div_power?(a,n,y)(m)
    IMPLIES
    LET sigx = sign_ext(polynomial(a,n)(x)), sigz = sign_ext(polynomial(a,n)(z)) IN
      sigx/=0 AND sigz/=0 AND
      ((even?(m) AND (NOT odd?(m)) AND sigx = sigz AND sigx/=-sigz)
       OR
       (odd?(m) AND (NOT even?(m)) AND sigx = -sigz AND sigx/=sigz))

  poly_eq_except_on_finite_set: LEMMA FORALL (b:[nat->real]):
    FORALL (N:posnat): (EXISTS (rootseq:[below(N)->real]):
        FORALL (x): (FORALL (ib:below(N)): x/=rootseq(ib)) IMPLIES
    polynomial(a,n)(x)=polynomial(b,m)(x))
    IMPLIES ((FORALL (j:nat): j<=n AND j>min(n,m) IMPLIES a(j)=0) AND
         (FORALL (j:nat): j<=m AND j>min(n,m) IMPLIES b(j)=0) AND
     (FORALL (j:nat): j<=min(n,m) IMPLIES a(j) = b(j)) AND
     polynomial(a,n) = polynomial(b,m))

  max_div_linear_power_remainder_sign_swaps: LEMMA
    FORALL (p,q,h,r:[nat->real],pn,qn,hn,rn:nat,m,kp:posnat):
    x<y AND y<z AND
    (FORALL (xyz:real): polynomial(p,pn)(xyz)=
      polynomial(q,qn)(xyz)*polynomial(h,hn)(xyz)
        +polynomial(r,rn)(xyz)) AND
    (FORALL (xyz:real): x<=xyz AND xyz<=z AND
      (polynomial(p,pn)(xyz)=0 OR polynomial(h,hn)(xyz)=0 OR polynomial(r,rn)(xyz)=0)
      IMPLIES xyz = y) AND
    max_linear_div_power?(p,pn,y)(m) AND
    max_linear_div_power?(r,rn,y)(m) AND
    max_linear_div_power?(h,hn,y)(kp) AND
    kp>m
    IMPLIES
    (sign_ext(polynomial(p,pn)(x))*sign_ext(polynomial(-r,rn)(x)) = -1 AND
     sign_ext(polynomial(p,pn)(z))*sign_ext(polynomial(-r,rn)(z)) = -1)

  at_zero_remainder_sign_swaps: LEMMA
    FORALL (p,q,h,r:[nat->real],pn,qn,hn,rn:nat):
    x<=y AND y<=z AND
    (FORALL (xyz:real): polynomial(p,pn)(xyz)=
      polynomial(q,qn)(xyz)*polynomial(h,hn)(xyz)
        +polynomial(r,rn)(xyz)) AND
    (FORALL (xyz:real): x<=xyz AND xyz<=z AND
      (polynomial(p,pn)(xyz)=0 OR polynomial(h,hn)(xyz)=0 OR polynomial(r,rn)(xyz)=0)
      IMPLIES xyz = y) AND
   polynomial(h,hn)(y)=0 AND
   polynomial(p,pn)(y)/=0 AND
   polynomial(r,rn)(y)/=0 AND
   polynomial(p,pn)(x)/=0 AND
   polynomial(r,rn)(x)/=0 AND
   polynomial(p,pn)(z)/=0 AND
   polynomial(r,rn)(z)/=0
    IMPLIES
    (sign_ext(polynomial(p,pn)(x))*sign_ext(polynomial(-r,rn)(x)) = -1 AND
     sign_ext(polynomial(p,pn)(z))*sign_ext(polynomial(-r,rn)(z)) = -1)

  %%% All derivatives vanish %%%

  poly_all_derivs_vanish: LEMMA
    (FORALL (i:nat): i<=n IMPLIES polynomial(poly_n_deriv(a,n-i),i)(x)=0)
    IFF
    (FORALL (i:nat): i<=n IMPLIES a(i)=0)

  %%% sign of polynomial values near infinity %%%

  poly_sign_near_infinity: LEMMA a(n)/=0 IMPLIES
    EXISTS (M:posnat): FORALL (x:real): x>=M IMPLIES
      sign_ext(polynomial(a,n)(x)) = sign_ext(a(n))

  poly_sign_near_negative_infinity: LEMMA a(n)/=0 IMPLIES
    EXISTS (M:posnat): FORALL (x:real): x<=-M IMPLIES
      sign_ext(polynomial(a,n)(x)) = sign_ext(IF even?(n) THEN a(n) ELSE -a(n) ENDIF)

  poly_coeff_bound(a,n): RECURSIVE {kr:posreal |
    FORALL (i:nat): i<=n IMPLIES abs(a(i))<kr} =
      IF n = 0 THEN abs(a(0))+1
      ELSE max(abs(a(n))+1,poly_coeff_bound(a,n-1))
      ENDIF MEASURE n

  poly_continuity_const(a,n,x,(epsil:posreal)): posreal =
    IF n = 0 THEN 1/2 ELSE
      LET epcon = epsil/(poly_coeff_bound(a,n) *
                  (sigma(1,n,LAMBDA (i:nat): sigma(1,i,LAMBDA (j:nat): IF (j=0 OR j>i) THEN 0
                ELSE C(i,j-1)*abs(x)^(j-1) ENDIF)) + 1))
      IN min(epcon,1/2)
    ENDIF

  poly_continuity_const_def: LEMMA FORALL (epsil:posreal):
      LET delt = poly_continuity_const(a,n,x,epsil)
      IN  FORALL (y:real): abs(x-y)<delt IMPLIES
         abs(polynomial(a,n)(y)-polynomial(a,n)(x))<epsil

  max_nonvanishing_deriv(a,n,x):
    RECURSIVE {lastn:nat | lastn <= n AND
            ((EXISTS (ii:upto(n)): a(ii)/=0)
            IMPLIES (polynomial(poly_n_deriv(a,n-lastn),lastn)(x)/=0 AND
            FORALL (i:nat): i>lastn AND i<=n IMPLIES
          polynomial(poly_n_deriv(a,n-i),i)(x)=0))} =
    IF n=0 OR polynomial(a,n)(x)/=0 THEN n
    ELSE max_nonvanishing_deriv(poly_deriv(a),n-1,x) ENDIF
    MEASURE n

  poly_rootless_width(a,n,x,(nzb: bool | nzb
          IFF (EXISTS (i:upto(n)): a(i)/=0))): posreal =
    LET maxn = max_nonvanishing_deriv(a,n,x)
    IN  IF nzb THEN poly_continuity_const(poly_n_deriv(a,n-maxn),maxn,x,
                  abs(polynomial(poly_n_deriv(a,n-maxn),maxn)(x)))
     ELSE 1 ENDIF

  poly_rootless_width_def: LEMMA
    (EXISTS (i:upto(n)): a(i)/=0) IMPLIES
    LET epsil=poly_rootless_width(a,n,x,TRUE),
     mnd  =max_nonvanishing_deriv(a,n,x)
    IN  FORALL (y:real,j:nat): j<=n-mnd
          AND polynomial(poly_n_deriv(a,j),n-j)(y)=0 AND abs(x-y)<epsil
   IMPLIES x=y

  poly_roots_enumerated: LEMMA (EXISTS (i:upto(n)): a(i)/=0)
    IMPLIES EXISTS (M:nat,rootseq:[below(M)->real]):
      (FORALL (i:below(M)): polynomial(a,n)(rootseq(i))=0)
      AND (FORALL (x:real): polynomial(a,n)(x)=0 IMPLIES
            EXISTS (i:below(M)): x=rootseq(i)) AND injective?(rootseq)

  min_poly_root_distance: LEMMA (EXISTS (i:upto(n)): a(i)/=0)
    IMPLIES EXISTS (epsil:posreal): FORALL (x,y:real):
    polynomial(a,n)(x)=0 AND polynomial(a,n)(y)=0 AND x/=y IMPLIES
    abs(x-y)>=epsil

  min_poly_root_dist(a,(n|a(n)/=0)): {epsil:posreal|FORALL (x,y:real):
    polynomial(a,n)(x)=0 AND polynomial(a,n)(y)=0 AND x/=y IMPLIES
    abs(x-y)>epsil}

  % The bound below is very similar to Cauchy's bound.

  poly_root_bound(a,(n|a(n)/=0)): {K:posreal| FORALL (x:real):
    polynomial(a,n)(x)=0 IMPLIES abs(x) < K} =
      max(2,sigma(0,n-1,LAMBDA (i:nat): abs(a(i)))/abs(a(n)) + 1)

  poly_cancel: LEMMA (EXISTS (i:nat):i<=p AND h(i)/=0) AND
    (FORALL (x): polynomial(h,p)(x)*polynomial(a,n)(x) =
           polynomial(h,p)(x)*polynomial(b,m)(x)) IMPLIES
    polynomial(a,n)=polynomial(b,m)

  % In order to make Knuth's bound useful, we need a way to comp kth root.
  % We follow the method of de Moura

  Knuth_bound_simple: LEMMA FORALL (r:real):
    a(n)=1 AND polynomial(a,n)(r)=0 AND r>0 AND n>0 IMPLIES
    EXISTS (k:subrange(1,n)): a(n-k)<0 AND r^k <= - 2^k * a(n-k)

  Knuth_poly_pos_root_bound(a,(n|a(n)=1 AND n>0)): {K:real| FORALL (x:real):
    polynomial(a,n)(x)=0 AND x>0 IMPLIES x <= K} =
      LET maxKfun = (LAMBDA (k:nat): IF 1<=k AND k<=n AND a(n-k)<0
                   THEN LET aquot = -a(n-k),
               log2j = least_pow_2_ge(aquot),
    rootexp = floor(log2j/k)+1
       IN 2^rootexp
                       ELSE -1 ENDIF)
      IN 2*max_rec(maxKfun,1,n)

  Knuth_poly_root_bound(a,(n|a(n)/=0)): {K:nnreal| FORALL (x:real):
    polynomial(a,n)(x)=0 IMPLIES abs(x) <= K} =
      IF n=0 THEN 0
      ELSE
        LET negsign = (LAMBDA (i:nat): IF even?(i) THEN 1 ELSE -1 ENDIF),
     nega = (LAMBDA (i:nat): negsign(i)*negsign(n)*a(i)/a(n)),
     newa = (LAMBDA (i:nat): a(i)/a(n)),
     negbound = Knuth_poly_pos_root_bound(nega,n),
     posbound = Knuth_poly_pos_root_bound(newa,n)
        IN max(posbound,max(negbound,0))
      ENDIF

  Knuth_poly_root_strict_bound(a,(n|a(n)/=0)): {K:posreal| FORALL (x:real):
    polynomial(a,n)(x)=0 IMPLIES abs(x) < K} =
      LET Kprb = Knuth_poly_root_bound(a,n) IN
        IF    Kprb=0 THEN 1
        ELSIF polynomial(a,n)(Kprb)=0 OR polynomial(a,n)(-Kprb)=0 THEN 1.01*Kprb
ELSE  Kprb ENDIF


  poly_increasing_is_strict: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) >= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) < polynomial(a,n)(y)))

  poly_increasing_is_strict2: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) >= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) <= polynomial(a,n)(y)))

  poly_decreasing_is_strict: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) <= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) > polynomial(a,n)(y)))

  poly_decreasing_is_strict2: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (c:real): xlb <= c AND c <= yub IMPLIES polynomial(poly_deriv(a),n-1)(c) <= 0)
    IFF
    (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) >= polynomial(a,n)(y)))

  poly_injective_monotone: LEMMA FORALL (xlb,yub:real):
    xlb < yub AND n > 0 AND a(n)/=0 IMPLIES
    ((FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) /= polynomial(a,n)(y))
    IFF
    ((FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) > polynomial(a,n)(y)) OR
     (FORALL (x,y:real): xlb <= x AND x<y AND y<=yub IMPLIES polynomial(a,n)(x) < polynomial(a,n)(y))))

  % Max root is like max_linear_div_power, but more robust.

  root_degree(a,n)(y): RECURSIVE {m| m<=n AND (a(n)/=0 IMPLIES
    ((EXISTS (b:[nat->real]): (FORALL (x): polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
      polynomial(b,n-m)(y)/=0 AND b(n-m)/=0) AND
    (polynomial(a,n)(y)=0 IMPLIES m>0) AND
    ((n>0 AND m>0) IMPLIES (EXISTS (q:[nat->real]): (FORALL (x): polynomial(poly_deriv(a),n-1)(x) =
             (x-y)^(m-1)*polynomial(q,n-m)(x)) AND
      polynomial(q,n-m)(y)/=0))))} =
    IF polynomial(a,n)(y)/=0 OR n=0 THEN 0
    ELSE 1+root_degree(poly_shift(LAMBDA (i:nat): poly_shift(a,n)(y)(i+1),n-1)(-y),n-1)(y)
    ENDIF MEASURE n

  root_degree_pos: LEMMA a(n)/=0 IMPLIES
    (polynomial(a,n)(y)=0 IFF root_degree(a,n)(y)>0)

  root_degree_max_linear_div_power: LEMMA a(n)/=0 AND
    (polynomial(a,n)(y)=0 OR root_degree(a,n)(y)>0) IMPLIES
     max_linear_div_power?(a,n,y)(root_degree(a,n)(y))

  root_degree_unique: LEMMA
    a(n)/=0 AND m<=n AND (EXISTS (b:[nat->real]): (FORALL (x):
      polynomial(a,n)(x)=(x-y)^m*polynomial(b,n-m)(x)) AND
      polynomial(b,n-m)(y)/=0) IMPLIES
      m = root_degree(a,n)(y)

  only_root_between?(a,n,x,y)(z): bool =
    x<z AND z<y AND
    (FORALL (r:real): x<=r AND r<=y AND r/=z IMPLIES
      polynomial(a,n)(r)/=0)

  root_degree_odd: LEMMA a(n)/=0 AND only_root_between?(a,n,x,y)(z) IMPLIES
    (odd?(root_degree(a,n)(z)) IFF sign_ext(polynomial(a,n)(x))=
                 -sign_ext(polynomial(a,n)(y)))

  root_degree_even: LEMMA a(n)/=0 AND only_root_between?(a,n,x,y)(z) IMPLIES
    (even?(root_degree(a,n)(z)) IFF sign_ext(polynomial(a,n)(x))=
                 sign_ext(polynomial(a,n)(y)))

  root_degree_deriv: LEMMA a(n)/=0 AND polynomial(a,n)(y)=0 AND n>0 IMPLIES
    root_degree(poly_deriv(a),n-1)(y) = root_degree(a,n)(y)-1

  root_degree_mult: LEMMA a(n)/=0 AND b(m)/=0 IMPLIES
    root_degree(polynomial_prod(a,n,b,m),n+m)(y) = root_degree(a,n)(y)+root_degree(b,m)(y)

  root_degree_scal: LEMMA a(n)/=0 AND x/=0 IMPLIES
    root_degree(x*a,n)(y) = root_degree(a,n)(y)

  root_degree_power_linear: LEMMA
    root_degree(power_linear(-y, 1, m),m)(y) = m

  root_degree_eq: LEMMA a(n)/=0 AND
    (FORALL (i:upto(n)): a(i)=b(i)) IMPLIES
    root_degree(a,n)(y) = root_degree(b,n)(y)

  root_degree_lower_bound: LEMMA FORALL (k:nat):
    a(n)/=0 AND (EXISTS (b:[nat->real]): b(k)/=0 AND (FORALL (x):
      polynomial(a,n)(x)=(x-y)^m*polynomial(b,k)(x))) IMPLIES
      (k=n-m AND root_degree(a,n)(y)>=m)

  root_degree_division: LEMMA
    FORALL (a,b,g,h:[nat->real],n,m,k,p:nat):
    (FORALL (x:real): polynomial(a,n)(x) =
   polynomial(g,k)(x)*polynomial(b,m)(x)
     + polynomial(h,p)(x)) AND h(p)/=0 AND
    a(n)/=0 AND b(m)/=0 IMPLIES
    ((root_degree(a,n)(y)<root_degree(b,m)(y) IMPLIES
      root_degree(h,p)(y)=root_degree(a,n)(y)) AND
     root_degree(h,p)(y)>=
     min(root_degree(a,n)(y),root_degree(b,m)(y)))

  signs_swap_division: LEMMA
    FORALL (a,b,g,h:[nat->real],n,m,k,p:nat):
    only_root_between?(a,n,x,y)(z) AND
    only_root_between?(b,m,x,y)(z) AND
    only_root_between?(h,p,x,y)(z) AND
    (FORALL (r:real): polynomial(a,n)(r) =
   polynomial(g,k)(r)*polynomial(b,m)(r)
     + polynomial(h,p)(r)) AND h(p)/=0 AND
    a(n)/=0 AND b(m)/=0 AND
    root_degree(a,n)(z)=root_degree(h,p)(z) AND
    root_degree(b,m)(z)>=root_degree(h,p)(z) IMPLIES
     ((sign_ext(polynomial(a,n)(x))*sign_ext(polynomial(h,p)(x))=1 AND
       sign_ext(polynomial(a,n)(y))*sign_ext(polynomial(h,p)(y))=1) OR
       (EXISTS (sig:Sign): (FORALL (abh:[nat->real],kz:nat):
         ((abh=a AND kz=n) OR (abh=b AND kz=m) OR (abh=h AND kz=p)) IMPLIES
  sign_ext(polynomial(abh,kz)(x)) = sig*sign_ext(polynomial(abh,kz)(y)))))

END more_polynomial_props

quality62%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.

more_polynomial_props.pvs Interaktion und PortierbarkeitPVS

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Haftungshinweis

Bemerkung:

more_polynomial_props.pvs Interaktion und
PortierbarkeitPVS