|
sturm: THEORY
BEGIN
IMPORTING reals@polynomials,reals@more_polynomial_props,reals@sign,
polynomial_division,
structures@more_list_props,ints@gcd,
number_sign_changes,
structures@sort_array,gcd_coeff
a,r : VAR [nat->real]
p : VAR [nat->[nat->real]]
n : VAR [nat->nat]
d,m,i,j,k : VAR nat
x,y,c,b : VAR real
constructed_sturm_sequence?(p,n,m): bool =
(FORALL (i:below(m)): p(i)(n(i))/=0) AND
(FORALL (i,j:below(m)): i<j IMPLIES n(i)>n(j)) AND
p(1) = poly_deriv(p(0)) AND n(1) = 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
constructed_sturm_seq_repeated_root: LEMMA
constructed_sturm_sequence?(p,n,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)
constructed_sturm_seq_repeated_root_mth: LEMMA FORALL (mm:posnat):
constructed_sturm_sequence?(p,n,m) AND
max_linear_div_power?(p(0),n(0),y)(mm) AND
i<m AND mm>1 IMPLIES
FORALL (u:upto(i)):
EXISTS (kp:posnat): kp>=mm-1 AND
max_linear_div_power?(p(u),n(u),y)(kp)
constructed_sturm_seq_repeated_root_struct: LEMMA
constructed_sturm_sequence?(p,n,m) IMPLIES
FORALL (i:nat): i+1<=m AND
polynomial(p(i),n(i))(y)=0 AND polynomial(p(i+1),n(i+1))(y)=0
IMPLIES
EXISTS (mm:posnat): mm>1 AND max_linear_div_power?(p(0),n(0),y)(mm) AND
(FORALL (j:nat): (1<=j AND j<m-1 AND
(NOT max_linear_div_power?(p(j),n(j),y)(mm-1))) IMPLIES
(1<j AND max_linear_div_power?(p(j-1),n(j-1),y)(mm-1) AND
max_linear_div_power?(p(j+1),n(j+1),y)(mm-1))) AND
max_linear_div_power?(p(m-1),n(m-1),y)(mm-1)
sturm_sig(p,n,m)(x): nat = number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(x),m)`num
% Part 1: Proving Sturm's Theorem when f has no multiple roots
constructed_sturm_seq_first_signs_eq: LEMMA
x<b AND b<y AND
polynomial(p(0),n(0))(b)=0 AND
(FORALL (c:real): x<=c AND c<=y AND polynomial(p(0),n(0))(c)=0 IMPLIES
(polynomial(p(1),n(1))(c)/=0 AND c = b)) AND
constructed_sturm_sequence?(p,n,m)
IMPLIES
((x/=b IMPLIES polynomial(p(0),n(0))(x)/=0) AND
(y/=b IMPLIES polynomial(p(0),n(0))(y)/=0) AND
(x/=b IMPLIES sign_ext(polynomial(p(0),n(0))(x)) = -sign_ext(polynomial(p(1),n(1))(b))) AND
(y/=b IMPLIES sign_ext(polynomial(p(0),n(0))(y)) = sign_ext(polynomial(p(1),n(1))(b))))
sturm_lem_no_roots: LEMMA
x<y AND
(FORALL (c:real,i:nat): i<=m AND x<=c AND c<=y IMPLIES polynomial(p(i),n(i))(c)/=0)
IMPLIES
sturm_sig(p,n,m)(x) = sturm_sig(p,n,m)(y)
constructed_sturm_lem_one_simple_root: LEMMA
x<y AND x<b AND b<y AND
(FORALL (c:real,i:nat): i<=m-1 AND x<=c AND c<=y AND polynomial(p(i),n(i))(c)=0
IMPLIES c = b) AND
(polynomial(p(0),n(0))(b)=0 IMPLIES polynomial(p(1),n(1))(b)/=0) AND
constructed_sturm_sequence?(p,n,m)
IMPLIES
LET nsc = LAMBDA (xyz:real,pj:nat): number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(xyz),pj) IN
sign_ext(nsc(x,m-1)`lastnz) = sign_ext(nsc(y,m-1)`lastnz) AND
nsc(x,m-1)`num = nsc(y,m-1)`num+(IF polynomial(p(0),n(0))(b)=0 THEN 1 ELSE 0 ENDIF)
constructed_sturm_lem_one_multi_root: LEMMA
x<y AND x<b AND b<y AND
(FORALL (c:real,i:nat): i<=m-1 AND x<=c AND c<=y AND polynomial(p(i),n(i))(c)=0
IMPLIES c = b) AND
polynomial(p(0),n(0))(b)=0 AND polynomial(p(1),n(1))(b)=0 AND
constructed_sturm_sequence?(p,n,m)
IMPLIES
LET nsc = LAMBDA (xyz:real,pj:nat): number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(xyz),pj) IN
nsc(x,m-1)`num = nsc(y,m-1)`num+1
constructed_sturm_lem_edge_root: LEMMA
x<y AND (x=b OR y=b) AND
(FORALL (c:real,i:nat): i<=m-1 AND x<=c AND c<=y AND polynomial(p(i),n(i))(c)=0
IMPLIES c = b) AND
(polynomial(p(0),n(0))(b)=0 IMPLIES polynomial(p(1),n(1))(b)/=0) AND
constructed_sturm_sequence?(p,n,m)
IMPLIES
LET nsc = LAMBDA (xyz:real,pj:nat): number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(xyz),pj) IN
sign_ext(nsc(x,m-1)`lastnz) = sign_ext(nsc(y,m-1)`lastnz) AND
nsc(x,m-1)`num = nsc(y,m-1)`num+(IF b=y AND polynomial(p(0),n(0))(b)=0 THEN 1 ELSE 0 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,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))
constructed_sturm_lem_no_roots_full: LEMMA
x<y AND
(FORALL (c:real,i:nat): i<=m-1 AND x<c AND c<=y IMPLIES polynomial(p(i),n(i))(c)/=0) AND
constructed_sturm_sequence?(p,n,m) AND
(polynomial(p(0),n(0))(x)=0 IMPLIES
polynomial(p(1),n(1))(x)/=0)
IMPLIES
sturm_sig(p,n,m-1)(x) = sturm_sig(p,n,m-1)(y)
sturm: LEMMA
x<y AND
constructed_sturm_sequence?(p,n,m) AND
(polynomial(p(1),n(1))(x)/=0 OR polynomial(p(0),n(0))(x)/=0) AND
(polynomial(p(1),n(1))(y)/=0 OR polynomial(p(0),n(0))(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>=0 AND EXISTS (bij: [below(Nroots)->{xr:real|x<xr AND xr<=y AND polynomial(p(0),n(0))(xr)=0}]):
bijective?(bij)
sturm_unbounded_left: LEMMA
constructed_sturm_sequence?(p,n,m) AND
(polynomial(p(1),n(1))(y)/=0 OR polynomial(p(0),n(0))(y)/=0)
IMPLIES
LET nscy = number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(y),m-1),
nscninf = number_sign_changes(LAMBDA (i): (-1)^(n(i))*p(i)(n(i)),m-1),
Nroots = nscninf`num-nscy`num
IN Nroots>=0 AND EXISTS (bij: [below(Nroots)->{xr:real|xr<=y AND polynomial(p(0),n(0))(xr)=0}]):
bijective?(bij)
sturm_unbounded_right: LEMMA
constructed_sturm_sequence?(p,n,m) AND
(polynomial(p(1),n(1))(x)/=0 OR polynomial(p(0),n(0))(x)/=0)
IMPLIES
LET nscx = number_sign_changes(LAMBDA (i): polynomial(p(i),n(i))(x),m-1),
nscinf = number_sign_changes(LAMBDA (i): p(i)(n(i)),m-1),
Nroots = nscx`num-nscinf`num
IN Nroots>=0 AND EXISTS (bij: [below(Nroots)->{xr:real|xr>x AND polynomial(p(0),n(0))(xr)=0}]):
bijective?(bij)
sturm_unbounded: LEMMA
constructed_sturm_sequence?(p,n,m) IMPLIES
LET nschigh = number_sign_changes(LAMBDA (i): p(i)(n(i)),m-1),
nsclow = number_sign_changes(LAMBDA (i): (-1)^(n(i))*p(i)(n(i)),m-1),
Nroots = nsclow`num-nschigh`num
IN Nroots>=0 AND EXISTS (bij: [below(Nroots)->{xr:real|polynomial(p(0),n(0))(xr)=0}]):
bijective?(bij)
END sturm
¤ Dauer der Verarbeitung: 0.21 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.
|
