:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation
:: by Krzysztof Treyderowski and Christoph Schwarzweller
::
:: Copyright (c) 2006-2019 Association of Mizar Users

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 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
coherence
proof end;
end;

theorem Th2: :: POLYNOM8:2
for L being non empty right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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;

definition
end;

:: deftheorem POLYNOM8:def 2 :
canceled;

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;

definition
let L be non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr ;
let a be Element of L;
let i be Integer;
func pow (a,i) -> Element of L equals :Def2: :: POLYNOM8:def 3
() . (a,i) if 0 <= i
otherwise (() . (a,|.i.|)) " ;
coherence
( ( 0 <= i implies () . (a,i) is Element of L ) & ( not 0 <= i implies (() . (a,|.i.|)) " is Element of L ) )
proof end;
consistency
for b1 being Element of L holds verum
;
end;

:: deftheorem Def2 defines pow POLYNOM8:def 3 :
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for a being Element of L
for i being Integer holds
( ( 0 <= i implies pow (a,i) = () . (a,i) ) & ( not 0 <= i implies pow (a,i) = (() . (a,|.i.|)) " ) );

theorem Th13: :: POLYNOM8:13
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for x being Element of L holds pow (x,0) = 1. L
proof end;

Lm3: for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for a being Element of L
for i being Integer st 0 > i holds
pow (a,i) = (pow (a,|.i.|)) "

proof end;

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

proof end;

theorem Th14: :: POLYNOM8:14
for L being non empty almost_left_invertible well-unital distributive associative commutative 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 well-unital distributive associative commutative doubleLoopStr
for x being Element of L holds pow (x,(- 1)) = x "
proof end;

Lm5: for L being non empty almost_left_invertible well-unital distributive associative commutative 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 well-unital distributive associative commutative 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 well-unital distributive associative commutative 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 well-unital distributive associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 left-distributive well-unital add-associative right_zeroed associative commutative 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 left-distributive well-unital add-associative right_zeroed associative commutative 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 well-unital distributive associative commutative 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 well-unital distributive add-associative right_zeroed associative commutative 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 well-unital distributive associative commutative 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 well-unital distributive associative commutative 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 well-unital distributive associative commutative 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;

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 :Def3: :: 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)
proof end;
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
proof end;
end;

:: deftheorem Def3 defines mConv POLYNOM8:def 4 :
for m being Nat
for L being non empty ZeroStr
for p being AlgSequence of L
for b4 being Matrix of m,1,L holds
( b4 = mConv (p,m) iff for i being Nat st 1 <= i & i <= m holds
b4 * (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 :Def4: :: 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 b1 being AlgSequence of L st
( ( for i being Nat st i < len M holds
b1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b1 . i = 0. L ) )
proof end;
uniqueness
for b1, b2 being AlgSequence of L st ( for i being Nat st i < len M holds
b1 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b1 . i = 0. L ) & ( for i being Nat st i < len M holds
b2 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b2 . i = 0. L ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines aConv POLYNOM8:def 5 :
for L being non empty ZeroStr
for M being Matrix of L
for b3 being AlgSequence of L holds
( b3 = aConv M iff ( ( for i being Nat st i < len M holds
b3 . i = M * ((i + 1),1) ) & ( for i being Nat st i >= len M holds
b3 . i = 0. L ) ) );

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 :: 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 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
proof end;

theorem Th32: :: POLYNOM8:32
for L being non empty non degenerated right_complementable almost_left_invertible well-unital distributive add-associative right_zeroed associative commutative 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 :Def6: :: 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 b1 being AlgSequence of L st
( ( for i being Nat st i < m holds
b1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b1 . i = 0. L ) )
proof end;
uniqueness
for b1, b2 being AlgSequence of L st ( for i being Nat st i < m holds
b1 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b1 . i = 0. L ) & ( for i being Nat st i < m holds
b2 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b2 . i = 0. L ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 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 b5 being AlgSequence of L holds
( b5 = DFT (p,x,m) iff ( ( for i being Nat st i < m holds
b5 . i = eval (p,(x |^ i)) ) & ( for i being Nat st i >= m holds
b5 . 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 well-unital distributive associative commutative doubleLoopStr ;
let m be Nat;
let x be Element of L;
func Vandermonde (x,m) -> Matrix of m,L means :Def7: :: 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)))
proof end;
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
proof end;
end;

:: deftheorem Def7 defines Vandermonde POLYNOM8:def 8 :
for L being non empty almost_left_invertible well-unital distributive associative commutative doubleLoopStr
for m being Nat
for x being Element of L
for b4 being Matrix of m,L holds
( b4 = Vandermonde (x,m) iff for i, j being Nat st 1 <= i & i <= m & 1 <= j & j <= m holds
b4 * (i,j) = pow (x,((i - 1) * (j - 1))) );

notation
let L be non empty almost_left_invertible well-unital distributive associative commutative 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;

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;

:: Multiplication of Polynomials using Discrete Fourier Transformation
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;