|
poly_systems: THEORY
BEGIN
% Systems of Polynomials
IMPORTING reals@polynomials,reals@more_polynomial_props,reals@sign,reals@real_orders,
structures@sort_array,tarski_query_matrix
a,r,g : VAR [nat->int]
p : VAR [nat->[nat->int]]
relseq: VAR [nat->RealOrder]
n : VAR [nat->nat]
d,i,j,k : VAR nat
m: VAR posnat
%m : VAR posnat
x,y,c,b : VAR real
babove,bbelow,bbelow2,babove2: VAR bool
RelF6,TQRow: VAR [nat->subrange(0,5)]
system_roots_enum: LEMMA
(FORALL (i):i<=k IMPLIES p(i)(n(i))/=0) IMPLIES
EXISTS (K:nat,enum:[below(K)->real]):
(FORALL (i,j:below(K)): i<j IMPLIES enum(i)<enum(j)) AND
(FORALL (i:below(K)): EXISTS (j): j<=k AND polynomial(p(j),n(j))(enum(i))=0) AND
(FORALL (b,j): j<=k AND polynomial(p(j),n(j))(b)=0 IMPLIES
EXISTS (i:below(K)): b = enum(i))
strict_poly_system_solvable: LEMMA (FORALL (i):i<=k IMPLIES p(i)(n(i))/=0) IMPLIES
((EXISTS (x): FORALL (i): i<=k IMPLIES polynomial(p(i),n(i))(x)>0)
IFF
((FORALL (i): i<=k IMPLIES p(i)(n(i))>0) OR
(FORALL (i): i<=k IMPLIES (IF odd?(n(i)) THEN -1 ELSE 1 ENDIF)*p(i)(n(i))>0) OR
(EXISTS (x): (LET Q = prod_polynomials(p,n,(LAMBDA (i:nat): 1),k),Qdeg = sigma(0,k,n) IN
Qdeg>0 AND polynomial(poly_deriv(Q),Qdeg-1)(x)=0) AND FORALL (i): i<=k
IMPLIES polynomial(p(i),n(i))(x)>0)))
% The following function computes the number of solutions to poly(a,m)(x)=0
% AND poly(p(i),n(i))(x)>0 for i<=k. Another version will be formed below.
A63_tensor_power_mat_row(m)(RelF6): RECURSIVE {M:PosFullMatrix|rows(M)=1 AND columns(M)=3^m} =
IF m = 1 THEN vect2matrix(row(A63)(RelF6(0)))
ELSE tensor_prod(A63_tensor_power_mat_row(m-1)((LAMBDA (d): RelF6(d+1))),
vect2matrix(row(A63)(RelF6(0))))
ENDIF MEASURE m
A63_tensor_power_mat_row_def: LEMMA
LET ii = base_n_to_nat(6,RelF6,k) IN
A63_tensor_power_mat_row(1+k)(RelF6) =
vect2matrix(row(tensor_power_alt(A63,1+k))(ii))
sturm_tarski_solver_slow_basic(k,a,(m|a(m)/=0),p,
(n|FORALL (i:upto(k)):p(i)(n(i))/=0),RelF6):
{r:real | r = NSol_all(k,a,m,p,n,RelF6) AND rational_pred(r) AND integer_pred(r)} =
super_dot(row(A63_tensor_power_mat_row(k+1)(RelF6))(0),col(TQ_vect3k(k,a,m,p,n))(0))
END poly_systems
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Laden
Fehler beim Verzeichnis:
in der Quellcodebibliothek suchen
Die farbliche Syntaxdarstellung ist noch experimentell.
|
