:: 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

begin

Lm1: for j being Integer holds
( j >= 0 or j = - 1 or j < - 1 )

proof end;

Lm2: for j being Integer holds
( j >= 1 or j = 0 or j < 0 )

proof end;

theorem Th1: :: POLYNOM8:1

for n being Element of NAT
for L being non empty non degenerated well-unital domRing-like doubleLoopStr
for x being Element of L st x <> 0. L holds
x |^ n <> 0. L

proof end;

registration

cluster non empty right_complementable almost_left_invertible associative right-distributive well-unital add-associative right_zeroed -> non empty right_complementable associative right-distributive well-unital add-associative right_zeroed domRing-like doubleLoopStr ;
coherence
for b₁ being non empty right_complementable associative right-distributive well-unital add-associative right_zeroed doubleLoopStr st b₁ is almost_left_invertible holds
b₁ is domRing-like

proof end;

end;

theorem Th2: :: POLYNOM8:2

for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for x, y being Element of L st x <> 0. L & y <> 0. L holds
(x * y) " = (x " ) * (y " )

proof end;

theorem Th3: :: POLYNOM8:3

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for z, z1 being Element of L st z <> 0. L holds
z1 = (z1 * z) / z

proof end;

theorem Th4: :: POLYNOM8:4

for L being non empty right_complementable add-associative right_zeroed left_zeroed doubleLoopStr
for m being Element of NAT
for s being FinSequence of L st len s = m & ( for k being Element of NAT st 1 <= k & k <= m holds
s /. k = 1. L ) holds
Sum s = m * (1. L)

proof end;

theorem Th5: :: POLYNOM8:5

for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for s being FinSequence of L
for q being Element of L st q <> 1. L & ( for i being Nat st 1 <= i & i <= len s holds
s . i = q |^ (i -' 1) ) holds
Sum s = ((1. L) - (q |^ (len s))) / ((1. L) - q)

proof end;

definition

let L be non empty well-unital doubleLoopStr ;
let m be Element of NAT ;
func emb m,L -> Element of L equals :: POLYNOM8:def 1
m * (1. L);
coherence
m * (1. L) is Element of L ;

end;

:: deftheorem defines emb POLYNOM8:def 1 :

for L being non empty well-unital doubleLoopStr
for m being Element of NAT holds emb m,L = m * (1. L);

theorem Th6: :: POLYNOM8:6

for L being Field
for m, n, k being Element of NAT st m > 0 & n > 0 holds
for M1 being Matrix of m,n,L
for M2 being Matrix of n,k,L holds ((emb m,L) * M1) * M2 = (emb m,L) * (M1 * M2)

proof end;

theorem Th7: :: POLYNOM8:7

for L being non empty ZeroStr
for p being AlgSequence of L
for i being Element of NAT st p . i <> 0. L holds
len p >= i + 1

proof end;

theorem Th8: :: POLYNOM8:8

for L being non empty ZeroStr
for s being AlgSequence of L st len s > 0 holds
s . ((len s) - 1) <> 0. L

proof end;

theorem Th9: :: POLYNOM8:9

for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed domRing-like doubleLoopStr
for p, q being Polynomial of L st len p > 0 & len q > 0 holds
len (p *' q) <= (len p) + (len q)

proof end;

theorem Th10: :: POLYNOM8:10

for L being non empty associative doubleLoopStr
for k, l being Element of L
for seq being sequence of L holds k * (l * seq) = (k * l) * seq

proof end;

begin

definition

let L be non empty doubleLoopStr ;
let m1, m2 be sequence of L;
func m1 * m2 -> sequence of L means :Def2: :: POLYNOM8:def 2
for i being Nat holds it . i = (m1 . i) * (m2 . i);
existence
ex b₁ being sequence of L st
for i being Nat holds b₁ . i = (m1 . i) * (m2 . i)

proof end;

uniqueness
for b₁, b₂ being sequence of L st ( for i being Nat holds b₁ . i = (m1 . i) * (m2 . i) ) & ( for i being Nat holds b₂ . i = (m1 . i) * (m2 . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines * POLYNOM8:def 2 :

for L being non empty doubleLoopStr
for m1, m2, b₄ being sequence of L holds
( b₄ = m1 * m2 iff for i being Nat holds b₄ . i = (m1 . i) * (m2 . i) );

registration

let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ;
let m1, m2 be AlgSequence of L;
cluster m1 * m2 -> finite-Support ;
coherence
m1 * m2 is finite-Support

proof end;

end;

theorem Th11: :: POLYNOM8:11

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for m1, m2 being AlgSequence of L holds len (m1 * m2) <= min (len m1),(len m2)

proof end;

theorem :: POLYNOM8:12

for L being non empty right_complementable distributive add-associative right_zeroed domRing-like doubleLoopStr
for m1, m2 being AlgSequence of L st len m1 = len m2 holds
len (m1 * m2) = len m1

proof end;

begin

definition

let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let a be Element of L;
let i be Integer;
func pow a,i -> Element of L equals :Def3: :: POLYNOM8:def 3
(power L) . a,i if 0 <= i
otherwise ((power L) . a,(abs i)) " ;
coherence
( ( 0 <= i implies (power L) . a,i is Element of L ) & ( not 0 <= i implies ((power L) . a,(abs i)) " is Element of L ) )

proof end;

consistency
for b₁ being Element of L holds verum ;

end;

:: deftheorem Def3 defines pow POLYNOM8:def 3 :

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for a being Element of L
for i being Integer holds
( ( 0 <= i implies pow a,i = (power L) . a,i ) & ( not 0 <= i implies pow a,i = ((power L) . a,(abs i)) " ) );

theorem Th13: :: POLYNOM8:13

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L holds pow x,0 = 1. L

proof end;

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)) "

proof end;

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)) "

proof end;

theorem Th14: :: POLYNOM8:14

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L holds pow x,1 = x

proof end;

theorem Th15: :: POLYNOM8:15

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L holds pow x,(- 1) = x "

proof end;

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

proof end;

theorem Th16: :: POLYNOM8:16

for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for i being Integer holds pow (1. L),i = 1. L

proof end;

theorem Th17: :: POLYNOM8:17

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for n being Element of NAT holds
( pow x,(n + 1) = (pow x,n) * x & pow x,(n + 1) = x * (pow x,n) )

proof end;

Lm6: for L being non empty well-unital doubleLoopStr
for n being Element of NAT holds (1. L) |^ n = 1. L

proof end;

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

proof end;

theorem Th18: :: POLYNOM8:18

for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for i being Integer
for x being Element of L st x <> 0. L holds
(pow x,i) " = pow x,(- i)

proof end;

theorem Th19: :: POLYNOM8:19

for L being Field
for j being Integer
for x being Element of L st x <> 0. L holds
pow x,(j + 1) = (pow x,j) * (pow x,1)

proof end;

theorem Th20: :: POLYNOM8:20

for L being Field
for j being Integer
for x being Element of L st x <> 0. L holds
pow x,(j - 1) = (pow x,j) * (pow x,(- 1))

proof end;

theorem Th21: :: POLYNOM8:21

for L being Field
for i, j being Integer
for x being Element of L st x <> 0. L holds
(pow x,i) * (pow x,j) = pow x,(i + j)

proof end;

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) "

proof end;

theorem Th22: :: POLYNOM8:22

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
pow (x " ),k = pow x,(- k)

proof end;

theorem Th23: :: POLYNOM8:23

for L being Field
for x being Element of L st x <> 0. L holds
for i, j, k being Nat holds (pow x,((i - 1) * (k - 1))) * (pow x,(- ((j - 1) * (k - 1)))) = pow x,((i - j) * (k - 1))

proof end;

theorem Th24: :: POLYNOM8:24

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for n, m being Element of NAT holds pow x,(n * m) = pow (pow x,n),m

proof end;

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) "

proof end;

theorem Th25: :: POLYNOM8:25

for L being Field
for x being Element of L st x <> 0. L holds
for i being Integer holds pow (x " ),i = (pow x,i) "

proof end;

theorem Th26: :: POLYNOM8:26

for L being Field
for x being Element of L st x <> 0. L holds
for i, j being Integer holds pow x,(i * j) = pow (pow x,i),j

proof end;

theorem Th27: :: POLYNOM8:27

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for x being Element of L
for i, k being Element of NAT st 1 <= k holds
pow x,(i * (k - 1)) = pow (x |^ i),(k - 1)

proof end;

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

proof end;

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

proof end;

begin

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 b₁ being Matrix of m,1,L st
for i being Nat st 1 <= i & i <= m holds
b₁ * i,1 = p . (i - 1)

proof end;

uniqueness
for b₁, b₂ being Matrix of m,1,L st ( for i being Nat st 1 <= i & i <= m holds
b₁ * i,1 = p . (i - 1) ) & ( for i being Nat st 1 <= i & i <= m holds
b₂ * i,1 = p . (i - 1) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines mConv POLYNOM8:def 4 :

for m being Nat
for L being non empty ZeroStr
for p being AlgSequence of L
for b₄ being Matrix of m,1,L holds
( b₄ = mConv p,m iff for i being Nat st 1 <= i & i <= m holds
b₄ * i,1 = p . (i - 1) );

theorem Th28: :: POLYNOM8:28

for m being Nat st m > 0 holds
for L being non empty ZeroStr
for p being AlgSequence of L holds
( len (mConv p,m) = m & width (mConv p,m) = 1 & ( for i being Nat st i < m holds
(mConv p,m) * (i + 1),1 = p . i ) )

proof end;

theorem Th29: :: POLYNOM8:29

for m being Nat st m > 0 holds
for L being non empty ZeroStr
for a being AlgSequence of L
for M being Matrix of m,1,L st ( for i being Nat st i < m holds
M * (i + 1),1 = a . i ) holds
mConv a,m = M

proof end;

definition

let L be non empty ZeroStr ;
let M be Matrix of L;
func aConv M -> AlgSequence of L means :Def5: :: POLYNOM8:def 5
( ( for i being Nat st i < len M holds
it . i = M * (i + 1),1 ) & ( for i being Nat st i >= len M holds
it . i = 0. L ) );
existence
ex b₁ being AlgSequence of L st
( ( for i being Nat st i < len M holds
b₁ . i = M * (i + 1),1 ) & ( for i being Nat st i >= len M holds
b₁ . i = 0. L ) )

proof end;

uniqueness
for b₁, b₂ being AlgSequence of L st ( for i being Nat st i < len M holds
b₁ . i = M * (i + 1),1 ) & ( for i being Nat st i >= len M holds
b₁ . i = 0. L ) & ( for i being Nat st i < len M holds
b₂ . i = M * (i + 1),1 ) & ( for i being Nat st i >= len M holds
b₂ . i = 0. L ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines aConv POLYNOM8:def 5 :

for L being non empty ZeroStr
for M being Matrix of L
for b₃ being AlgSequence of L holds
( b₃ = aConv M iff ( ( for i being Nat st i < len M holds
b₃ . i = M * (i + 1),1 ) & ( for i being Nat st i >= len M holds
b₃ . i = 0. L ) ) );

begin

definition

let L be non empty well-unital doubleLoopStr ;
let x be Element of L;
let n be Element of NAT ;
pred x is_primitive_root_of_degree n means :Def6: :: POLYNOM8:def 6
( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds
x |^ i <> 1. L ) );

end;

:: deftheorem Def6 defines is_primitive_root_of_degree POLYNOM8:def 6 :

for L being non empty well-unital doubleLoopStr
for x being Element of L
for n being Element of NAT holds
( x is_primitive_root_of_degree n iff ( n <> 0 & x |^ n = 1. L & ( for i being Element of NAT st 0 < i & i < n holds
x |^ i <> 1. L ) ) );

theorem Th30: :: POLYNOM8:30

for L being non empty non degenerated right_complementable right-distributive well-unital add-associative right_zeroed doubleLoopStr
for n being Element of NAT holds not 0. L is_primitive_root_of_degree n

proof end;

theorem Th31: :: POLYNOM8:31

for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
x " is_primitive_root_of_degree m

proof end;

theorem Th32: :: POLYNOM8:32

for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr
for m being Element of NAT
for x being Element of L st x is_primitive_root_of_degree m holds
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m & i <> j holds
pow x,(i - j) <> 1. L

proof end;

definition

let m be Nat;
let L be non empty well-unital doubleLoopStr ;
let p be Polynomial of L;
let x be Element of L;
func DFT p,x,m -> AlgSequence of L means :Def7: :: POLYNOM8:def 7
( ( for i being Nat st i < m holds
it . i = eval p,(x |^ i) ) & ( for i being Nat st i >= m holds
it . i = 0. L ) );
existence
ex b₁ being AlgSequence of L st
( ( for i being Nat st i < m holds
b₁ . i = eval p,(x |^ i) ) & ( for i being Nat st i >= m holds
b₁ . i = 0. L ) )

proof end;

uniqueness
for b₁, b₂ being AlgSequence of L st ( for i being Nat st i < m holds
b₁ . i = eval p,(x |^ i) ) & ( for i being Nat st i >= m holds
b₁ . i = 0. L ) & ( for i being Nat st i < m holds
b₂ . i = eval p,(x |^ i) ) & ( for i being Nat st i >= m holds
b₂ . i = 0. L ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def7 defines DFT POLYNOM8:def 7 :

for m being Nat
for L being non empty well-unital doubleLoopStr
for p being Polynomial of L
for x being Element of L
for b₅ being AlgSequence of L holds
( b₅ = DFT p,x,m iff ( ( for i being Nat st i < m holds
b₅ . i = eval p,(x |^ i) ) & ( for i being Nat st i >= m holds
b₅ . i = 0. L ) ) );

theorem Th33: :: POLYNOM8:33

for m being Nat
for L being non empty well-unital doubleLoopStr
for x being Element of L holds DFT (0_. L),x,m = 0_. L

proof end;

theorem Th34: :: POLYNOM8:34

for m being Nat
for L being Field
for p, q being Polynomial of L
for x being Element of L holds (DFT p,x,m) * (DFT q,x,m) = DFT (p *' q),x,m

proof end;

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 b₁ being Matrix of m,L st
for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b₁ * i,j = pow x,((i - 1) * (j - 1))

proof end;

uniqueness
for b₁, b₂ being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b₁ * i,j = pow x,((i - 1) * (j - 1)) ) & ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b₂ * i,j = pow x,((i - 1) * (j - 1)) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines Vandermonde POLYNOM8:def 8 :

for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr
for m being Nat
for x being Element of L
for b₄ being Matrix of m,L holds
( b₄ = Vandermonde x,m iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b₄ * i,j = pow x,((i - 1) * (j - 1)) );

notation

let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ;
let m be Nat;
let x be Element of L;
synonym VM x,m for Vandermonde x,m;

end;

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

proof end;

theorem Th36: :: POLYNOM8:36

for L being Field
for m being Element of NAT st 0 < m holds
for u, v, u1 being Matrix of m,L st ( for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
(u * v) * i,j = (emb m,L) * (u1 * i,j) ) holds
u * v = (emb m,L) * u1

proof end;

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))

proof end;

theorem Th37: :: POLYNOM8:37

for L being Field
for x being Element of L
for s being FinSequence of L
for i, j, m being Element of NAT st x is_primitive_root_of_degree m & 1 <= i & i <= m & 1 <= j & j <= m & len s = m & ( for k being Nat st 1 <= k & k <= m holds
s /. k = pow x,((i - j) * (k - 1)) ) holds
((VM x,m) * (VM (x " ),m)) * i,j = Sum s

proof end;

theorem Th38: :: POLYNOM8:38

for L being Field
for m, i, j being Element of NAT
for x being Element of L st i <> j & 1 <= i & i <= m & 1 <= j & j <= m & x is_primitive_root_of_degree m holds
((VM x,m) * (VM (x " ),m)) * i,j = 0. L

proof end;

theorem Th39: :: POLYNOM8:39

for L being Field
for m being Element of NAT st m > 0 holds
for x being Element of L st x is_primitive_root_of_degree m holds
(VM x,m) * (VM (x " ),m) = (emb m,L) * (1. L,m)

proof end;

theorem Th40: :: POLYNOM8:40

for L being Field
for m being Element of NAT
for x being Element of L st m > 0 & x is_primitive_root_of_degree m holds
(VM x,m) * (VM (x " ),m) = (VM (x " ),m) * (VM x,m)

proof end;

begin

theorem Th41: :: POLYNOM8:41

for L being Field
for p being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m holds
for x being Element of L
for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1

proof end;

theorem Th42: :: POLYNOM8:42

for L being Field
for p being Polynomial of L
for m being Nat st 0 < m & len p <= m holds
for x being Element of L holds DFT p,x,m = aConv ((VM x,m) * (mConv p,m))

proof end;

theorem Th43: :: POLYNOM8:43

for L being Field
for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m holds
DFT (DFT (p *' q),x,(2 * m)),(x " ),(2 * m) = (emb (2 * m),L) * (p *' q)

proof end;

theorem :: POLYNOM8:44

for L being Field
for p, q being Polynomial of L
for m being Element of NAT st m > 0 & len p <= m & len q <= m holds
for x being Element of L st x is_primitive_root_of_degree 2 * m & emb (2 * m),L <> 0. L holds
((emb (2 * m),L) " ) * (DFT ((DFT p,x,(2 * m)) * (DFT q,x,(2 * m))),(x " ),(2 * m)) = p *' q

proof end;