POLYNOM2: Evaluation of Multivariate Polynomials

:: Evaluation of Multivariate Polynomials
:: by Christoph Schwarzweller and Andrzej Trybulec
::
:: Received April 14, 2000
:: Copyright (c) 2000-2011 Association of Mizar Users

begin

Lm1: for X being set
for A being Subset of X
for O being Order of X holds
( O is_reflexive_in A & O is_antisymmetric_in A & O is_transitive_in A )

proof end;

Lm2: for X being set
for A being Subset of X
for O being Order of X st O is_connected_in X holds
O is_connected_in A

proof end;

Lm3: for X being set
for S being Subset of X
for R being Order of X st R is being_linear-order holds
R linearly_orders S

proof end;

theorem :: POLYNOM2:1

canceled;

theorem Th2: :: POLYNOM2:2

for L being non empty unital associative multMagma
for a being Element of L
for n, m being Element of NAT holds (power L) . (a,(n + m)) = ((power L) . (a,n)) * ((power L) . (a,m))

proof end;

registration

cluster non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ;
existence

proof end;

end;

begin

theorem :: POLYNOM2:3

canceled;

theorem Th4: :: POLYNOM2:4

for p being FinSequence
for k being Element of NAT st k in dom p holds
for i being Element of NAT st 1 <= i & i <= k holds
i in dom p

proof end;

Lm4: for X being set
for A being finite Subset of X
for a being Element of X
for R being Order of X st R linearly_orders {a} \/ A holds
R linearly_orders A

proof end;

theorem Th5: :: POLYNOM2:5

for L being non empty right_zeroed left_zeroed addLoopStr
for p being FinSequence of the carrier of L
for 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

proof end;

theorem :: POLYNOM2:6

for L being non empty right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for 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

proof end;

theorem Th7: :: POLYNOM2:7

for L being non empty Abelian add-associative addLoopStr
for a being Element of L
for 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)

proof end;

theorem Th8: :: POLYNOM2:8

for L being non empty associative commutative doubleLoopStr
for a being Element of L
for 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)

proof end;

theorem Th9: :: POLYNOM2:9

for X being set
for A being empty Subset of X
for R being Order of X st R linearly_orders A holds
SgmX (R,A) = {}

proof end;

theorem Th10: :: POLYNOM2:10

for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, j being Element of NAT st i in dom (SgmX (R,A)) & j in dom (SgmX (R,A)) & (SgmX (R,A)) /. i = (SgmX (R,A)) /. j holds
i = j

proof end;

Lm5: for D being set
for p being FinSequence of D st dom p <> {} holds
1 in dom p

proof end;

theorem Th11: :: POLYNOM2:11

for X being set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX (R,B)) & (SgmX (R,B)) /. k = a holds
for i being Element of NAT st 1 <= i & i <= k - 1 holds
(SgmX (R,B)) /. i = (SgmX (R,A)) /. i

proof end;

theorem Th12: :: POLYNOM2:12

for X being set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k in dom (SgmX (R,B)) & (SgmX (R,B)) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX (R,A)) holds
(SgmX (R,B)) /. (i + 1) = (SgmX (R,A)) /. i

proof end;

theorem Th13: :: POLYNOM2:13

for X being non empty set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX (R,B)) & (SgmX (R,B)) /. (k + 1) = a holds
SgmX (R,B) = Ins ((SgmX (R,A)),k,a)

proof end;

begin

theorem Th14: :: POLYNOM2:14

for X being set
for b being bag of X st support b = {} holds
b = EmptyBag X

proof end;

Lm6: for X being set
for b being bag of X holds b is PartFunc of X,NAT

proof end;

definition

let X be set ;
let b be bag of X;
attr b is empty means :Def1: :: POLYNOM2:def 1
b = EmptyBag X;

end;

:: deftheorem Def1 defines empty POLYNOM2:def 1 :

registration

let X be non empty set ;
cluster Relation-like X -defined Function-like total V198() V199() V200() V201() V202() V203() finite-support non empty set ;
existence

proof end;

end;

definition

let X be set ;
let b be bag of X;
:: original: support
redefine func support b -> finite Subset of X;
coherence

proof end;

end;

theorem Th15: :: POLYNOM2:15

for n being Ordinal
for b being bag of n holds RelIncl n linearly_orders support b

proof end;

definition

let X be set ;
let x be FinSequence of X;
let b be bag of X;
:: original: *
redefine func b * x -> PartFunc of NAT,NAT;
coherence

proof end;

end;

definition

let n be Ordinal;
let b be bag of n;
let L be non empty non trivial well-unital doubleLoopStr ;
let x be Function of n,L;
func eval (b,x) -> Element of L means :Def2: :: 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)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines eval POLYNOM2:def 2 :

Lm7: for X being set holds support (EmptyBag X) = {}

proof end;

theorem Th16: :: POLYNOM2:16

for n being Ordinal
for L being non empty non trivial well-unital doubleLoopStr
for x being Function of n,L holds eval ((EmptyBag n),x) = 1. L

proof end;

theorem Th17: :: POLYNOM2:17

for n being Ordinal
for L being non empty non trivial well-unital doubleLoopStr
for u being set
for b being bag of n st support b = {u} holds
for x being Function of n,L holds eval (b,x) = (power L) . ((x . u),(b . u))

proof end;

Lm8: for n being Ordinal
for L being non empty non trivial right_complementable associative commutative add-associative right_zeroed well-unital distributive doubleLoopStr
for b1, b2 being bag of n
for u being set st not u in support b1 & support b2 = (support b1) \/ {u} & ( for u9 being set st u9 <> u holds
b2 . u9 = b1 . u9 ) holds
for x being Function of n,L
for a being Element of L st a = (power L) . ((x . u),(b2 . u)) holds
eval (b2,x) = a * (eval (b1,x))

proof end;

Lm9: for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for b1 being bag of n st ex u being set st support b1 = {u} holds
for b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))

proof end;

theorem Th18: :: POLYNOM2:18

for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for b1, b2 being bag of n
for x being Function of n,L holds eval ((b1 + b2),x) = (eval (b1,x)) * (eval (b2,x))

proof end;

begin

registration

let n be Ordinal;
let L be non empty right_complementable add-associative right_zeroed addLoopStr ;
let p, q be Polynomial of n,L;
cluster p - q -> finite-Support ;
coherence

proof end;

end;

theorem Th19: :: POLYNOM2:19

for L being non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for n being Ordinal
for p being Polynomial of n,L st Support p = {} holds
p = 0_ (n,L)

proof end;

registration

let n be Ordinal;
let L be non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let p be Polynomial of n,L;
cluster Support p -> finite ;
coherence by POLYNOM1:def 10;

end;

theorem Th20: :: POLYNOM2:20

for n being Ordinal
for L being non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L holds BagOrder n linearly_orders Support p

proof end;

definition

let n be Ordinal;
let b be Element of Bags n;
func b @ -> bag of n equals :: POLYNOM2:def 3
b;
correctness ;

end;

:: deftheorem defines @ POLYNOM2:def 3 :

definition

let n be Ordinal;
let L be non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr ;
let p be Polynomial of n,L;
let x be Function of n,L;
func eval (p,x) -> Element of L means :Def4: :: 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)) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines eval POLYNOM2:def 4 :

theorem Th21: :: POLYNOM2:21

proof end;

theorem Th22: :: POLYNOM2:22

for n being Ordinal
for L being non empty non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L holds eval ((0_ (n,L)),x) = 0. L

proof end;

theorem Th23: :: POLYNOM2:23

proof end;

theorem Th24: :: POLYNOM2:24

proof end;

Lm10: for n being Ordinal
for L being non empty non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for x being Function of n,L
for b being bag of n st not b in Support p & Support q = (Support p) \/ {b} & ( for b9 being bag of n st b9 <> b holds
q . b9 = p . b9 ) holds
eval (q,x) = (eval (p,x)) + ((q . b) * (eval (b,x)))

proof end;