|
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
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.
|
