:: Diophantine sets -- Preliminaries
:: by Karol P\kak
::
:: Received March 27, 2018
:: Copyright (c) 2018-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, RELAT_1, ORDINAL4, FINSEQ_1, XBOOLE_0,
BINOP_1, FUNCT_1, FINSOP_1, XXREAL_0, TARSKI, NAT_1, INT_1, ARYTM_3,
ORDERS_1, FINSET_1, ZFMISC_1, CARD_1, PARTFUN1, ORDINAL1, RELAT_2,
ARYTM_1, FUNCOP_1, PBOOLE, CARD_3, VALUED_0, FUNCT_2, PRE_POLY, XCMPLX_0,
WELLORD2, QC_LANG1, GROUP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES,
STRUCT_0, SUPINF_2, MESFUNC1, RFINSEQ, POLYNOM1, ALGSEQ_1, POLYNOM2,
HILBASIS, GRAPH_2, AFINSQ_1, HILB10_2;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, RELAT_1,
XXREAL_0, XCMPLX_0, RELAT_2, FUNCT_1, PBOOLE, RELSET_1, FINSET_1,
PARTFUN1, FUNCT_2, FINSOP_1, FINSEQ_1, FUNCT_3, BINOP_1, XREAL_0,
ORDERS_1, FUNCOP_1, NAT_1, INT_1, VALUED_0, FINSEQOP, ALGSTR_0, RLVECT_1,
VFUNCT_1, VECTSP_1, GROUP_1, GROUP_4, RECDEF_1, PRE_POLY, POLYNOM1,
POLYNOM2, BAGORDER, HILBASIS, AFINSQ_1, AFINSQ_2, STRUCT_0;
constructors SETWISEO, FINSEQOP, FINSOP_1, RFUNCT_3, RECDEF_1, BINOP_2,
CLASSES1, RELSET_1, DOMAIN_1, GROUP_4, VFUNCT_1, POLYNOM2, BAGORDER,
HILBASIS, AFINSQ_2;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XREAL_0, NAT_1,
CARD_1, FINSEQ_1, VALUED_0, RELSET_1, FUNCT_2, INT_1, RFUNCT_2, STRUCT_0,
VECTSP_1, POLYNOM1, PRE_POLY, VFUNCT_1, MEMBERED, PRE_CIRC, POLYNOM2,
GROUP_1, FVSUM_1, AFINSQ_2, HILBASIS, BAGORDER, AFINSQ_1, NUMBERS;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
reserve i,j,k,n,m for Nat,
b,b1,b2 for bag of n;
registration
let X be non empty set;
let n be Nat;
cluster n-element for XFinSequence of X;
end;
registration
let n be Nat;
cluster n-element real-valued for XFinSequence;
end;
registration
let n,m be Nat;
let p be n-element XFinSequence;
let q be m-element XFinSequence;
cluster p^q -> (n+m) -element;
end;
registration
let p be real-valued XFinSequence;
let q be real-valued XFinSequence;
cluster p^q -> real-valued;
end;
definition
let n be Nat;
let p be n-element real-valued XFinSequence;
func @p -> Function of n,F_Real equals
:: HILB10_2:def 1
p;
end;
definition
let n be Nat;
let X be non empty set;
let p be Function of n,X;
func @p -> n-element XFinSequence of X equals
:: HILB10_2:def 2
p;
end;
registration
let X be set, p be Permutation of X, M be ManySortedSet of X;
cluster M * p -> total;
end;
registration
let F be finite-support Function;
let f be one-to-one Function;
cluster F*f -> finite-support;
end;
theorem :: HILB10_2:1
for F, G being XFinSequence st F^G is one-to-one holds
rng F misses rng G;
theorem :: HILB10_2:2
for X being set, f being X-defined Function,
perm being Permutation of X holds
card support (f*perm) = card support (f);
registration
let X be set;
cluster 0_(X, F_Real) -> natural-valued;
cluster 1_(X, F_Real) -> natural-valued;
end;
registration
let X be set;
let x be Element of X;
cluster 1_1(x,F_Real) -> natural-valued;
end;
registration
let X be set;
cluster INT -valued for Series of X,F_Real;
end;
registration
let O be Ordinal;
cluster INT -valued for Polynomial of O,F_Real;
end;
registration
let X be set, p be INT -valued Series of X, F_Real;
cluster -p -> INT -valued;
let q be INT -valued Series of X, F_Real;
cluster p+q ->INT -valued;
cluster p-q ->INT -valued;
end;
registration
let X be Ordinal, p,q be INT -valued Series of X, F_Real;
cluster p *' q ->INT -valued;
end;
registration
let X be set;
cluster natural-valued for Function of X, F_Real;
end;
registration
let O be Ordinal;
cluster INT -valued for Function of O, F_Real;
end;
registration
let O be Ordinal;
let b be bag of O;
let x be INT -valued Function of O, F_Real;
cluster eval(b,x) -> integer;
end;
registration
let O be Ordinal;
let p be INT -valued Polynomial of O,F_Real;
let x be INT -valued Function of O, F_Real;
cluster eval(p,x) -> integer;
end;
begin :: Polynomial extended by 0
theorem :: HILB10_2:3
for b being ManySortedSet of n st k <= n
holds (0,k)-cut b = b|k;
theorem :: HILB10_2:4
for b being bag of (n+1) holds
b = (0,n)-cut b bag_extend (b.n);
theorem :: HILB10_2:5
(0,n)-cut (b bag_extend k) = b;
definition
let n;
let L be non empty ZeroStr;
let p be Series of n,L;
func p extended_by_0 -> Series of n+1,L means
:: HILB10_2:def 3
for b being bag of n+1 holds
(b.n <>0 implies it.b = 0.L) &
(b.n = 0 implies it.b = p.(0,n)-cut b);
end;
theorem :: HILB10_2:6
for L being non empty ZeroStr, p being Series of n,L holds
(p extended_by_0).(b bag_extend 0) = p.b;
theorem :: HILB10_2:7
for L being non empty ZeroStr, p being Series of n,L,
b being bag of n+1 st b in Support (p extended_by_0)
holds b.n = 0;
theorem :: HILB10_2:8
for L being non empty ZeroStr, p being Series of n,L holds
b bag_extend 0 in Support (p extended_by_0) iff
b in Support p;
theorem :: HILB10_2:9
for L being non empty ZeroStr,
p being Series of n,L, b being bag of n+1 st b.n = 0 holds
b in Support (p extended_by_0) iff (0,n)-cut b in Support p;
registration
let n;
let L be non empty ZeroStr;
let p be Polynomial of n,L;
cluster p extended_by_0 -> finite-Support;
end;
theorem :: HILB10_2:10
for L being non empty ZeroStr,
p being Series of n,L holds
{0.L} \/ rng p = rng (p extended_by_0);
theorem :: HILB10_2:11
support b = support (b bag_extend 0);
theorem :: HILB10_2:12
SgmX(RelIncl n, support b) =
SgmX(RelIncl (n+1), support (b bag_extend 0));
theorem :: HILB10_2:13
for L being well-unital non trivial doubleLoopStr
for x being Function of n, L, y be Function of n+1,L st y|n = x
holds
eval(b,x) = eval(b bag_extend 0,y);
theorem :: HILB10_2:14
b1 < b2 iff b1 bag_extend k < b2 bag_extend k;
theorem :: HILB10_2:15
for X being non empty set,
A being finite Subset of X,
R being Order of X st R linearly_orders A
for i,k st 1 <= i <= k <= card A holds
SgmX(R, rng (SgmX(R,A)|k))/.i = SgmX(R,A)/.i;
theorem :: HILB10_2:16
for O being Ordinal,
A being finite Subset of Bags O st
n in dom SgmX(BagOrder O, A) & m in dom SgmX(BagOrder O, A) & n < m
holds SgmX(BagOrder O, A)/.n < SgmX(BagOrder O, A)/.m;
theorem :: HILB10_2:17
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr
for p being Polynomial of n,L
holds
len SgmX(BagOrder n, Support p) =
len SgmX(BagOrder (n+1), Support (p extended_by_0)) &
for i be Nat st 1<=i<= len SgmX(BagOrder n, Support p) holds
SgmX(BagOrder (n+1), Support (p extended_by_0))/.i =
SgmX(BagOrder n, Support p)/.i bag_extend 0;
theorem :: HILB10_2:18
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p being Polynomial of n,L,
x being Function of n, L,
y being Function of (n+1), L st y|n=x
holds eval(p,x) = eval(p extended_by_0,y);
begin :: Polynomial permuted by perm
theorem :: HILB10_2:19
for O being Ordinal, L being well-unital commutative associative non trivial
doubleLoopStr, x being Function of O, L, b being bag of O
for S being one-to-one FinSequence of O st
rng S = support b
ex y being FinSequence of L st
len y = card support b &
eval(b,x) = Product y &
for i st 1 <= i & i <= len y holds
y/.i = power(L).((x*S)/.i, (b*S)/.i);
theorem :: HILB10_2:20
for O being Ordinal,
L being well-unital commutative associative non trivial
doubleLoopStr, x being Function of O, L, b being bag of O
for perm being Permutation of O holds
eval(b,x) = eval(b*perm,x*perm);
definition
let O be Ordinal;
let L be non empty ZeroStr;
let s be Series of O,L;
let perm be Permutation of O;
func s permuted_by perm -> Series of O,L means
:: HILB10_2:def 4
for b being bag of O holds it.b = s.(b*perm);
end;
theorem :: HILB10_2:21
for O being Ordinal,
L being non empty ZeroStr,
perm being Permutation of O,
s being Series of O,L, b being bag of O holds
b in Support (s permuted_by perm) iff b*perm in Support s;
theorem :: HILB10_2:22
for O being Ordinal,
L being non empty ZeroStr,
perm being Permutation of O,
s being Series of O,L, b being bag of O holds
b*perm" in Support (s permuted_by perm) iff b in Support s;
theorem :: HILB10_2:23
for O being Ordinal,
L being non empty ZeroStr,
perm being Permutation of O,
s being Series of O,L holds
card Support s = card Support (s permuted_by perm);
theorem :: HILB10_2:24
for O being Ordinal,
L being Abelian right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p being Polynomial of O,L,
x being Function of O, L
for S being one-to-one FinSequence of Bags O st
rng S = Support p
ex y being FinSequence of L st
len y = card Support p &
eval(p,x) = Sum y &
for i being Nat st 1 <= i & i <= len y holds
y/.i = (p * S)/.i * eval(S/.i,x);
registration
let O be Ordinal;
let L be non empty ZeroStr;
let perm be Permutation of O;
let p be Polynomial of O,L;
cluster p permuted_by perm -> finite-Support;
end;
theorem :: HILB10_2:25
for O being Ordinal,
L being Abelian right_zeroed add-associative right_complementable
well-unital distributive commutative associative non trivial
doubleLoopStr,
p being Polynomial of O,L,
x being Function of O, L
for perm being Permutation of O holds
eval(p,x) = eval(p permuted_by perm,x*perm");
theorem :: HILB10_2:26
for O being Ordinal,
L being non empty ZeroStr,
s being Series of O,L,
perm being Permutation of O holds
rng (s permuted_by perm) = rng s;
begin :: Main Lemmas
theorem :: HILB10_2:27
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr,
p being Polynomial of n,L
ex q being Polynomial of n+m,L st
rng q c= rng p \/ {0.L}&
for x being Function of n, L,
y being Function of (n+m), L st y|n=x
holds eval(p,x) = eval(q,y);
theorem :: HILB10_2:28
for L being Abelian right_zeroed add-associative
right_complementable well-unital distributive commutative
associative non trivial doubleLoopStr,
p being Polynomial of n+m,L
ex q being Polynomial of n+k+m,L st
rng q c= rng p \/{0.L}&
for XY being Function of n+m,L,
XanyY being Function of n+k+m,L st
XY|n = XanyY|n&@XY/^n = @XanyY/^(n+k)
holds eval(p,XY) = eval(q,XanyY);
begin :: Diophantine Sets
reserve x,s for object;
definition
let D be non empty set;
let n be Nat;
func n -xtuples_of D -> Subset of D^omega means
:: HILB10_2:def 5
x in it iff x is n-element XFinSequence of D;
end;
registration
let D be non empty set;
let n be Nat;
cluster n -xtuples_of D -> non empty;
cluster -> n-element D-valued for Element of n -xtuples_of D;
end;
definition
let n be Nat;
let A be Subset of n -xtuples_of NAT;
attr A is diophantine means
:: HILB10_2:def 6
ex m being Nat, p being INT -valued Polynomial of n+m,F_Real st
for s holds
s in A iff ex x being n-element XFinSequence of NAT,
y being m-element XFinSequence of NAT st
s = x & eval(p,@(x^y)) = 0;
end;
registration
let n be Nat;
cluster empty -> diophantine for Subset of n-xtuples_of NAT;
cluster [#](n-xtuples_of NAT) -> diophantine;
end;
registration
let n be zero Nat;
cluster -> diophantine for Subset of n -xtuples_of NAT;
end;
registration
let n be Nat;
cluster non empty diophantine for Subset of n-xtuples_of NAT;
cluster empty diophantine for Subset of n-xtuples_of NAT;
end;
registration
let n be Nat;
let A,B be diophantine Subset of n -xtuples_of NAT;
cluster A /\ B -> diophantine for Subset of n -xtuples_of NAT;
cluster A \/ B -> diophantine for Subset of n -xtuples_of NAT;
end;