Quelle  sturm.pvs

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