:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation
:: by Krzysztof Treyderowski and Christoph Schwarzweller
::
:: Received October 12, 2006
:: Copyright (c) 2006 Association of Mizar Users
Lm1:
for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )
Lm2:
for j being Integer holds
( j >= 1 or j = 0 or j < 0 )
theorem Th1: :: POLYNOM8:1
theorem Th2: :: POLYNOM8:2
theorem Th3: :: POLYNOM8:3
theorem Th4: :: POLYNOM8:4
theorem Th5: :: POLYNOM8:5
:: deftheorem defines emb POLYNOM8:def 1 :
theorem Th6: :: POLYNOM8:6
theorem Th7: :: POLYNOM8:7
theorem Th8: :: POLYNOM8:8
theorem Th9: :: POLYNOM8:9
theorem Th10: :: POLYNOM8:10
:: deftheorem Def2 defines * POLYNOM8:def 2 :
theorem Th11: :: POLYNOM8:11
theorem :: POLYNOM8:12
:: deftheorem Def3 defines pow POLYNOM8:def 3 :
theorem Th13: :: POLYNOM8:13
Lm3:
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for a being Element of L
for i being Integer st 0 > i holds
pow a,i = (pow a,(abs i)) "
Lm4:
for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for i being Integer
for x being Element of L st i <= 0 holds
pow x,i = (pow x,(abs i)) "
theorem Th14: :: POLYNOM8:14
theorem Th15: :: POLYNOM8:15
Lm5:
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for i being Element of NAT holds pow (1. L),i = 1. L
theorem Th16: :: POLYNOM8:16
theorem Th17: :: POLYNOM8:17
Lm6:
for L being non empty well-unital doubleLoopStr
for n being Element of NAT holds (1. L) |^ n = 1. L
Lm7:
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for m being Element of NAT
for x being Element of L st x <> 0. L holds
(x |^ m) * ((x " ) |^ m) = 1. L
theorem Th18: :: POLYNOM8:18
theorem Th19: :: POLYNOM8:19
theorem Th20: :: POLYNOM8:20
theorem Th21: :: POLYNOM8:21
Lm8:
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr
for k being Element of NAT
for x being Element of L st x <> 0. L holds
(x " ) |^ k = (x |^ k) "
theorem Th22: :: POLYNOM8:22
theorem Th23: :: POLYNOM8:23
theorem Th24: :: POLYNOM8:24
Lm9:
for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for x being Element of L st x <> 0. L holds
for n being Element of NAT holds pow (x " ),n = (pow x,n) "
theorem Th25: :: POLYNOM8:25
theorem Th26: :: POLYNOM8:26
theorem Th27: :: POLYNOM8:27
Lm10:
for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for m being Element of NAT st x <> 0. L & x |^ m = 1. L holds
(x " ) |^ m = 1. L
Lm11:
for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for i being Element of NAT st x <> 0. L & (x " ) |^ i = 1. L holds
x |^ i = 1. L
definition
let m be
Nat;
let L be non
empty ZeroStr ;
let p be
AlgSequence of
L;
func mConv p,
m -> Matrix of
m,1,
L means :
Def4:
:: POLYNOM8:def 4
for
i being
Nat st 1
<= i &
i <= m holds
it * i,1
= p . (i - 1);
existence
ex b1 being Matrix of m,1,L st
for i being Nat st 1 <= i & i <= m holds
b1 * i,1 = p . (i - 1)
uniqueness
for b1, b2 being Matrix of m,1,L st ( for i being Nat st 1 <= i & i <= m holds
b1 * i,1 = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds
b2 * i,1 = p . (i - 1) ) holds
b1 = b2
end;
:: deftheorem Def4 defines mConv POLYNOM8:def 4 :
theorem Th28: :: POLYNOM8:28
theorem Th29: :: POLYNOM8:29
:: deftheorem Def5 defines aConv POLYNOM8:def 5 :
:: deftheorem Def6 defines is_primitive_root_of_degree POLYNOM8:def 6 :
theorem Th30: :: POLYNOM8:30
theorem Th31: :: POLYNOM8:31
theorem Th32: :: POLYNOM8:32
:: deftheorem Def7 defines DFT POLYNOM8:def 7 :
theorem Th33: :: POLYNOM8:33
theorem Th34: :: POLYNOM8:34
definition
let L be non
empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let m be
Nat;
let x be
Element of
L;
func Vandermonde x,
m -> Matrix of
m,
L means :
Def8:
:: POLYNOM8:def 8
for
i,
j being
Nat st 1
<= i &
i <= m & 1
<= j &
j <= m holds
it * i,
j = pow x,
((i - 1) * (j - 1));
existence
ex b1 being Matrix of m,L st
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b1 * i,j = pow x,((i - 1) * (j - 1))
uniqueness
for b1, b2 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b1 * i,j = pow x,((i - 1) * (j - 1)) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b2 * i,j = pow x,((i - 1) * (j - 1)) ) holds
b1 = b2
end;
:: deftheorem Def8 defines Vandermonde POLYNOM8:def 8 :
theorem Th35: :: POLYNOM8:35
for
L being
Field for
m,
n being
Nat st
m > 0 holds
for
M being
Matrix of
m,
n,
L holds
(1. L,m) * M = M
theorem Th36: :: POLYNOM8:36
Lm12:
for L being Field
for m being Element of NAT st m > 0 holds
for p, q being Polynomial of L holds (emb (2 * m),L) * ((1. L,(2 * m)) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (mConv (p *' q),(2 * m))
theorem Th37: :: POLYNOM8:37
theorem Th38: :: POLYNOM8:38
theorem Th39: :: POLYNOM8:39
theorem Th40: :: POLYNOM8:40
theorem Th41: :: POLYNOM8:41
theorem Th42: :: POLYNOM8:42
theorem Th43: :: POLYNOM8:43
theorem :: POLYNOM8:44