:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation
:: by Krzysztof Treyderowski and Christoph Schwarzweller
::
:: Received October 12, 2006
:: Copyright (c) 2006-2011 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;