:: Evaluation of Multivariate Polynomials
:: by Christoph Schwarzweller and Andrzej Trybulec
::
:: Received April 14, 2000
:: Copyright (c) 2000-2016 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, XBOOLE_0, SUBSET_1, FINSEQ_1, RELAT_1, PARTFUN1, CARD_1,
FUNCT_1, TARSKI, XXREAL_0, ARYTM_1, ARYTM_3, NAT_1, ORDERS_1, RELAT_2,
GROUP_1, BINOP_1, ALGSTR_0, RLVECT_1, VECTSP_1, LATTICES, ZFMISC_1,
FINSET_1, ALGSTR_1, STRUCT_0, SUPINF_2, CARD_3, FINSOP_1, ORDINAL4,
PRE_POLY, FINSEQ_5, FUNCT_4, FUNCOP_1, ORDINAL1, WELLORD2, MESFUNC1,
RFINSEQ, POLYNOM1, ALGSEQ_1, MSSUBFAM, QUOFIELD, POLYNOM2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
RELAT_1, FINSOP_1, RELAT_2, RELSET_1, FUNCT_1, FINSET_1, XCMPLX_0,
PARTFUN1, FUNCT_2, BINOP_1, FUNCT_4, FUNCT_7, REAL_1, NAT_1, ALGSTR_1,
ORDERS_1, FINSEQ_1, STRUCT_0, ALGSTR_0, RLVECT_1, FUNCOP_1, VFUNCT_1,
VECTSP_1, GROUP_1, GROUP_4, QUOFIELD, FINSEQ_5, GRCAT_1, RFINSEQ,
YELLOW_1, GROUP_6, XXREAL_0, RECDEF_1, PRE_POLY, POLYNOM1;
constructors REAL_1, FINSOP_1, RFINSEQ, BINARITH, FINSEQ_5, GROUP_4, GRCAT_1,
GROUP_6, MONOID_0, TRIANG_1, YELLOW_1, QUOFIELD, POLYNOM1, RECDEF_1,
ALGSTR_1, RELSET_1, FUNCT_7, FVSUM_1, VFUNCT_1, DOMAIN_1, RINGCAT1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0,
NAT_1, INT_1, FINSEQ_1, STRUCT_0, VECTSP_1, ALGSTR_1, MONOID_0, POLYNOM1,
VALUED_0, CARD_1, SUBSET_1, PRE_POLY, RELAT_1, VFUNCT_1, FUNCT_2,
FUNCT_1, PBOOLE, RINGCAT1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
begin
theorem :: POLYNOM2:1
for L being unital associative non empty multMagma, a being Element of L,
n,m being Element of NAT holds
power(L).(a,n+m) = power(L).(a,n) * power(L).(a,m);
registration
cluster Abelian right_zeroed add-associative right_complementable
well-unital distributive commutative associative for non trivial
doubleLoopStr;
end;
begin
::$CT
theorem :: POLYNOM2:3
for L being left_zeroed right_zeroed non empty addLoopStr, p
being FinSequence of the carrier of L, i being Element of NAT st i in dom p &
for i9 being Element of NAT st i9 in dom p & i9 <> i holds p/.i9 = 0.L holds
Sum p = p/.i;
theorem :: POLYNOM2:4
for L being add-associative right_zeroed right_complementable
distributive well-unital non empty doubleLoopStr, p being FinSequence of the
carrier of L st ex i being Element of NAT st i in dom p & p/.i = 0.L holds
Product p = 0.L;
theorem :: POLYNOM2:5
for L being Abelian add-associative non empty addLoopStr, a
being Element of L, p,q being FinSequence of the carrier of L st len p = len q
& ex i being Element of NAT st i in dom p & q/.i = a + p/.i & for i9 being
Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9 holds Sum q = a +
Sum p;
theorem :: POLYNOM2:6
for L being commutative associative non empty doubleLoopStr, a
being Element of L, p,q being FinSequence of the carrier of L st len p = len q
& ex i being Element of NAT st i in dom p & q/.i = a * p/.i & for i9 being
Element of NAT st i9 in dom p & i9 <> i holds q/.i9 = p/.i9 holds Product q = a
* Product p;
begin :: Evaluation of Bags -------------------------------------------------------
definition
::$CD
let n be Ordinal, b be bag of n, L be well-unital non trivial
doubleLoopStr, x be Function of n, L;
func eval(b,x) -> Element of L means
:: POLYNOM2:def 2
ex y being FinSequence of the carrier of L st
len y = len SgmX(RelIncl n, support b) & it = Product y &
for i being Element of NAT st 1 <= i & i <= len y holds
y/.i = power(L).((x * SgmX(RelIncl n, support b))/.i,
(b * SgmX(RelIncl n, support b))/.i);
end;
::$CT 7
theorem :: POLYNOM2:14
for n being Ordinal, L being well-unital non trivial
doubleLoopStr, x being Function of n, L holds eval(EmptyBag n,x) = 1.L;
theorem :: POLYNOM2:15
for n being Ordinal, L being well-unital non trivial
doubleLoopStr, u being set, b being bag of n st support b = {u} for x being
Function of n, L holds eval(b,x) = power(L).(x.u,b.u);
theorem :: POLYNOM2:16
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive Abelian non trivial commutative
associative non empty doubleLoopStr, b1,b2 being bag of n, x being Function
of n, L holds eval(b1+b2,x) = eval(b1,x) * eval(b2,x);
begin :: Evaluation of Polynomials ------------------------------------------------
registration
let n be Ordinal, L be add-associative right_zeroed right_complementable
non empty addLoopStr, p,q be Polynomial of n, L;
cluster p - q -> finite-Support;
end;
theorem :: POLYNOM2:17
for L being right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, n being Ordinal
, p being Polynomial of n,L st Support p = {} holds p = 0_(n,L);
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
of n,L;
cluster Support p -> finite;
end;
theorem :: POLYNOM2:18
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L holds BagOrder n linearly_orders
Support p;
definition
::$CD
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, p be Polynomial
of n,L, x be Function of n, L;
func eval(p,x) -> Element of L means
:: POLYNOM2:def 4
ex y being FinSequence of the
carrier of L st len y = len SgmX(BagOrder n, Support p) & it = Sum y & for i
being Element of NAT st 1 <= i & i <= len y holds y/.i = (p * SgmX(BagOrder n,
Support p))/.i * eval(((SgmX(BagOrder n, Support p))/.i),x);
end;
theorem :: POLYNOM2:19
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, p being Polynomial of n,L, b being bag of n st Support p = {b}
for x being Function of n, L holds eval(p,x) = p.b * eval(b,x);
theorem :: POLYNOM2:20
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, x being Function of n, L holds eval(0_(n,L),x) = 0.L;
theorem :: POLYNOM2:21
for n being Ordinal, L being right_zeroed add-associative
right_complementable well-unital distributive non trivial
doubleLoopStr, x being Function of n, L holds eval(1_(n,L),x) = 1.L;
theorem :: POLYNOM2:22
for n being Ordinal, 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 holds eval(
-p,x) = - eval(p,x);
theorem :: POLYNOM2:23
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, p,q being Polynomial of n,L, x being Function of n, L holds
eval(p+q,x) = eval(p,x) + eval(q,x);
theorem :: POLYNOM2:24
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial
doubleLoopStr, p,q being Polynomial of n,L, x being Function of n, L holds
eval(p-q,x) = eval(p,x) - eval(q,x);
theorem :: POLYNOM2:25
for n being Ordinal, L being right_zeroed add-associative
right_complementable Abelian well-unital distributive non trivial commutative
associative non empty doubleLoopStr, p,q being Polynomial of n,L, x being
Function of n, L holds eval(p*'q,x) = eval(p,x) * eval(q,x);
begin :: Evaluation Homomorphism --------------------------------------------------
definition
let n be Ordinal, L be right_zeroed add-associative right_complementable
well-unital distributive non trivial doubleLoopStr, x be Function
of n, L;
func Polynom-Evaluation(n,L,x) -> Function of Polynom-Ring(n,L),L means
:: POLYNOM2:def 5
for p being Polynomial of n,L holds it.p = eval(p,x);
end;
registration
let n be Ordinal, L be right_zeroed Abelian add-associative
right_complementable well-unital distributive associative non trivial non
empty doubleLoopStr;
cluster Polynom-Ring (n, L) -> well-unital;
end;
registration
let n be Ordinal, L be Abelian right_zeroed add-associative
right_complementable well-unital distributive associative non trivial non
empty doubleLoopStr, x be Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> unity-preserving;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive non trivial doubleLoopStr, x be
Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> additive;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
doubleLoopStr, x be Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> multiplicative;
end;
registration
let n be Ordinal, L be right_zeroed add-associative right_complementable
Abelian well-unital distributive commutative associative non trivial
doubleLoopStr, x be Function of n, L;
cluster Polynom-Evaluation(n,L,x) -> RingHomomorphism;
end;