|
sturmtarski: THEORY
BEGIN
% The proof of the theorem for the tarski query should be easier than
% for sturm's theorem, because one doesn't have to consider roots at the
% endpoints. Eventually, the endpoints will be pm infinity.
IMPORTING reals@polynomials,reals@more_polynomial_props,reals@sign,
Sturm@polynomial_division,Sturm@number_sign_changes,
structures@more_list_props,ints@gcd,
structures@sort_array,Sturm@gcd_coeff
a,r,g : VAR [nat->real]
p : VAR [nat->[nat->real]]
n : VAR [nat->nat]
d,i,j,k : VAR nat
m: VAR posnat
%m : VAR posnat
x,y,c,b : VAR real
rel: VAR [[real,real]->bool]
babove,bbelow,bbelow2,babove2: VAR bool
% k is the degree of g
constructed_sturm_sequence?(p,n,g,k,m): bool =
(FORALL (i:below(m)): p(i)(n(i))/=0) AND
(FORALL (i,j:subrange(1,m-1)): i<j IMPLIES n(i)>n(j)) AND
n(0)>0 AND
p(1) = polynomial_prod(g,k,poly_deriv(p(0)),n(0)-1) AND n(1) = k+n(0)-1 AND
n(m) = 0 AND p(m)(0) = 0 AND
(FORALL (j:nat): j>1 AND j<=m IMPLIES LET pd = poly_divide(p(j-2),n(j-2))(p(j-1),n(j-1))(0) IN
EXISTS (c:posreal):
polynomial(p(j),n(j)) =
polynomial(-c*pd`rem,pd`rdeg))
AND m>=2 AND g(k)/=0
constructed_sturm_seq_repeated_root: LEMMA
constructed_sturm_sequence?(p,n,g,k,m) IMPLIES
FORALL (i:nat): i+1<=m AND
polynomial(p(i),n(i))(x)=0 AND polynomial(p(i+1),n(i+1))(x)=0
IMPLIES
(FORALL (j:upto(m)): polynomial(p(j),n(j))(x) = 0)
default_root_degree?(p,n,g,k,m,y)(d): bool =
((d=0 AND root_degree(p(0),n(0))(y)=0 AND polynomial(p(0),n(0))(y)/=0 AND
polynomial(g,k)(y)/=0) OR
(root_degree(p(0),n(0))(y)=d+1 AND root_degree(p(1),n(1))(y)=d AND
polynomial(g,k)(y)/=0) OR
(root_degree(p(0),n(0))(y)=d AND root_degree(p(1),n(1))(y)=d AND
root_degree(g,k)(y)=1 AND polynomial(g,k)(y)=0) OR
(root_degree(p(0),n(0))(y)=d AND root_degree(p(1),n(1))(y)>d AND
root_degree(g,k)(y)>0 AND polynomial(g,k)(y)=0)) AND
(FORALL (i:nat): i<m AND root_degree(p(i),n(i))(y)/=d IMPLIES
((i>0 IMPLIES root_degree(p(i-1),n(i-1))(y)=d) AND
(i<m-1 IMPLIES root_degree(p(i+1),n(i+1))(y)=d))) AND
root_degree(p(m-1),n(m-1))(y)=d
constructed_sturm_seq_root_degrees: LEMMA
constructed_sturm_sequence?(p,n,g,k,m) IMPLIES
((polynomial(g,k)(y)=0 AND
default_root_degree?(p,n,g,k,m,y)(root_degree(p(0),n(0))(y))) OR
(polynomial(g,k)(y)/=0 AND
default_root_degree?(p,n,g,k,m,y)(max(root_degree(p(0),n(0))(y)-1,0))))
default_root_deg(p,n,g,k,m)(y): nat =
IF polynomial(g,k)(y)=0 THEN root_degree(p(0),n(0))(y)
ELSE max(root_degree(p(0),n(0))(y)-1,0) ENDIF
default_root_deg_def: LEMMA
constructed_sturm_sequence?(p,n,g,k,m) IMPLIES
default_root_degree?(p,n,g,k,m,y)(default_root_deg(p,n,g,k,m)(y))
constructed_sturm_seq_root_degree_lower_bound: LEMMA
constructed_sturm_sequence?(p,n,g,k,m) IMPLIES
FORALL (i): i<m IMPLIES root_degree(p(i),n(i))(y)>=default_root_deg(p,n,g,k,m)(y)
sturm_sig(p,n,m)(x): nat = number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(x),m)`num
sturm_tarski_basic_1: LEMMA FORALL (z:real):
constructed_sturm_sequence?(p,n,g,k,m) AND
(FORALL (j:below(m)): only_root_between?(p(j),n(j),x,y)(z)) AND
polynomial(p(0),n(0))(z)=0 AND polynomial(g,k)(z)/=0 IMPLIES
number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(x),1)`num -
number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(y),1)`num =
sign_ext(polynomial(g,k)(z))
sturm_tarski_basic_2: LEMMA FORALL (z:real):
LET nsc = (LAMBDA (xyz:real,k:nat):
number_sign_changes(LAMBDA (i):
polynomial(p(i),n(i))(xyz),k)`num)
IN root_degree(p(1),n(1))(z) = root_degree(p(0),n(0))(z) AND constructed_sturm_sequence?(p,n,g,k,m) AND
(FORALL (j:below(m)): only_root_between?(p(j),n(j),x,y)(z))
IMPLIES nsc(x,1)=nsc(y,1)
sturm_tarski_basic_3: LEMMA FORALL (z:real):
m>2 AND
constructed_sturm_sequence?(p,n,g,k,m) AND
(FORALL (j:below(m)): only_root_between?(p(j),n(j),x,y)(z)) AND
(polynomial(g,k)(z)=0 OR polynomial(p(0),n(0))(z)/=0) IMPLIES
LET nsc = (LAMBDA (xyz:real,k:nat):
number_sign_changes(LAMBDA (i):
polynomial(p(i),n(i))(xyz),k)`num)
IN (root_degree(p(2),n(2))(z) = root_degree(p(0),n(0))(z)
IMPLIES nsc(x,2)=nsc(y,2))
sturm_tarski_basic: LEMMA FORALL (z:real):
constructed_sturm_sequence?(p,n,g,k,m) AND
(FORALL (j:below(m)): only_root_between?(p(j),n(j),x,y)(z))
IMPLIES
number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(x),m-1)`num -
number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(y),m-1)`num =
(IF polynomial(p(0),n(0))(z)/=0 OR polynomial(g,k)(z)=0 THEN 0
ELSIF polynomial(g,k)(z)>0 THEN 1 ELSE -1 ENDIF)
constructed_sturm_roots_between_enum: LEMMA % THIS NEEDS TO BE FOR ALL P(i) NOT JUST P(0)
x<y AND constructed_sturm_sequence?(p,n,g,k,m) IMPLIES
EXISTS ((K:nat|K>=2),enum:[below(K)->real]):
(FORALL (i,j:below(K)): i<j IMPLIES enum(i)<enum(j)) AND
enum(0)=x AND enum(K-1)=y AND
(FORALL (b:real,j:nat): j<=m-1 AND x<b AND b<=y AND polynomial(p(j),n(j))(b)=0 IMPLIES
EXISTS (i:below(K)): b = enum(i))
Sol(a:[nat->real],(m:nat|a(m)/=0),g:[nat->real],k:nat,
rel:[[real,real]->bool],x,y:real,bbelow,babove:bool):
finite_set[real] = {r:real | polynomial(a,m)(r)=0 AND rel(polynomial(g,k)(r),0) AND
(bbelow IMPLIES x<=r) AND (babove IMPLIES r<=y)}
Sol_union_top: LEMMA FORALL (z:real): x<=y AND y<=z AND a(m)/=0 IMPLIES
union(Sol(a,m,g,k,rel,x,y,bbelow,babove),Sol(a,m,g,k,rel,y,z,bbelow2,babove2)) =
Sol(a,m,g,k,rel,x,z,bbelow AND bbelow2,babove AND babove2)
NSol(a:[nat->real],(m:nat|a(m)/=0),g:[nat->real],k:nat,
rel:[[real,real]->bool],x,y:real,bbelow,babove:bool): {d:nat |
EXISTS (enumsol:[below(d)->(Sol(a,m,g,k,rel,x,y,bbelow,babove))]):
bijective?(enumsol)} = card(Sol(a,m,g,k,rel,x,y,bbelow,babove))
NSol_union_top: LEMMA FORALL (z:real): x<=y AND y<=z AND a(m)/=0 AND
polynomial(a,m)(y)/=0 IMPLIES
NSol(a,m,g,k,rel,x,y,bbelow,True)+NSol(a,m,g,k,rel,y,z,True,babove) =
NSol(a,m,g,k,rel,x,z,bbelow,babove)
sturm_tarski: LEMMA
x<y AND
constructed_sturm_sequence?(p,n,g,k,m) AND
(FORALL (j:nat): j<m IMPLIES (polynomial(p(j),n(j))(x)/=0 AND polynomial(p(j),n(j))(y)/=0))
IMPLIES
LET nsc = LAMBDA (xyz:real): number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(xyz),m-1),
Nroots = nsc(x)`num-nsc(y)`num
IN Nroots = NSol(p(0),n(0),g,k,>,x,y,true,true)-NSol(p(0),n(0),g,k,<,x,y,true,true)
% Unbounded sets
Sol(a:[nat->real],(m:nat|a(m)/=0),g:[nat->real],k:nat,
rel:[[real,real]->bool]):
finite_set[real] = {r:real | polynomial(a,m)(r)=0 AND rel(polynomial(g,k)(r),0)}
NSol(a:[nat->real],(m:nat|a(m)/=0),g:[nat->real],k:nat,
rel:[[real,real]->bool]): {d:nat |
EXISTS (enumsol:[below(d)->(Sol(a,m,g,k,rel))]):
bijective?(enumsol)} = card(Sol(a,m,g,k,rel))
sturm_tarski_unbounded: LEMMA
constructed_sturm_sequence?(p,n,g,k,m) IMPLIES
LET nschigh = number_sign_changes(LAMBDA (i): p(i)(n(i)),m-1),
nsclow = number_sign_changes(LAMBDA (i): (IF even?(n(i)) THEN 1 ELSE -1 ENDIF)*p(i)(n(i)),m-1),
Nroots = nsclow`num-nschigh`num
IN Nroots = NSol(p(0),n(0),g,k,>)-NSol(p(0),n(0),g,k,<)
NSol_sq_gt: LEMMA a(m)/=0 IMPLIES
NSol(a,m,polynomial_prod(g,k,g,k),2*k,>) =
NSol(a,m,g,k,>) + NSol(a,m,g,k,<)
NSol_sq_lt: LEMMA a(m)/=0 IMPLIES
NSol(a,m,polynomial_prod(g,k,g,k),2*k,<) = 0
% constructed_sturm_sequence_p2: LEMMA
% constructed_sturm_sequence?(p,n,g,k,m) AND
% k>0 AND (m>2 OR k/=1 OR
% (NOT (k=1 AND EXISTS (r:real): root_degree(p(0),n(0))(r) = n(0) AND
% polynomial(g,1)(r)=0)))
% IMPLIES
% EXISTS (c:posreal):
% polynomial(p(2),n(2)) = polynomial(-c*p(0),n(0))
END sturmtarski
¤ Dauer der Verarbeitung: 0.16 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.
|
