:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation
:: by Krzysztof Treyderowski and Christoph Schwarzweller
::
:: Received October 12, 2006
:: Copyright (c) 2006-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, INT_1, XXREAL_0, CARD_1, ARYTM_1, ARYTM_3, SUBSET_1,
VECTSP_1, VECTSP_2, STRUCT_0, XBOOLE_0, ALGSTR_0, SUPINF_2, NEWTON,
RELAT_1, GROUP_1, BINOP_1, RLVECT_1, MESFUNC1, LATTICES, ALGSTR_1,
FINSEQ_1, PARTFUN1, CARD_3, NAT_1, FUNCT_1, ORDINAL4, FINSEQ_2, TARSKI,
MATRIX_1, TREES_1, INCSP_1, FVSUM_1, RVSUM_1, ZFMISC_1, ALGSEQ_1,
POLYNOM1, COMPLEX1, MCART_1, POLYNOM2, POLYNOM3, POLYNOM8;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, VECTSP_2, BINOP_1, BINOM, ALGSTR_1,
PARTFUN1, FINSEQ_1, FINSEQ_2, INT_1, NAT_1, NAT_D, STRUCT_0, ALGSTR_0,
RLVECT_1, GROUP_1, VECTSP_1, FVSUM_1, ALGSEQ_1, LOPBAN_3, POLYNOM5,
POLYNOM3, MATRIX_0, MATRIX_1, MATRIX_3, POLYNOM4, XTUPLE_0, MCART_1,
INT_2;
constructors REAL_1, NAT_D, VECTSP_2, ALGSTR_2, TOPREAL1, MATRIX_3, POLYNOM4,
POLYNOM5, BINOM, RELSET_1, FVSUM_1, XTUPLE_0, MATRIX_1, ALGSEQ_1,
BINOP_1, LOPBAN_3;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1,
STRUCT_0, VECTSP_1, ALGSTR_1, GCD_1, POLYNOM3, CARD_1, XTUPLE_0;
requirements NUMERALS, SUBSET, REAL, BOOLE, ARITHM;
begin
theorem :: POLYNOM8:1
for n being Nat, L being well-unital domRing-like non
degenerated non empty doubleLoopStr, x being Element of L st x <> 0.L holds x
|^ n <> 0.L;
registration
cluster almost_left_invertible -> domRing-like for associative well-unital
add-associative right_zeroed right_complementable right-distributive non empty
doubleLoopStr;
end;
theorem :: POLYNOM8:2
for L being add-associative right_zeroed right_complementable
associative commutative well-unital almost_left_invertible distributive non
empty doubleLoopStr, x,y being Element of L st x <> 0.L & y <> 0.L holds (x *
y)" = x" * y";
theorem :: POLYNOM8:3
for L being associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, z,z1 being Element of L holds
z <> 0.L implies z1 = (z1 * z) / z;
theorem :: POLYNOM8:4
for L being left_zeroed right_zeroed add-associative
right_complementable non empty doubleLoopStr, m being Element of NAT, 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;
theorem :: POLYNOM8:5
for L being add-associative right_zeroed right_complementable
associative commutative well-unital distributive almost_left_invertible non
empty doubleLoopStr, s being FinSequence of L, 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);
definition
let L be well-unital non empty doubleLoopStr, m be Element of NAT;
func emb(m,L) -> Element of L equals
:: POLYNOM8:def 1
m * 1.L;
end;
theorem :: POLYNOM8:6
for L being Field, m,n,k being Element of NAT st m > 0 & n > 0
for M1 being Matrix of m,n,L, M2 being Matrix of n,k,L holds (emb(m,L) * M1) *
M2 = emb(m,L) * (M1 * M2);
theorem :: POLYNOM8:7
for L being non empty ZeroStr, p being AlgSequence of L, i being
Element of NAT holds p.i <> 0.L implies len p >= i + 1;
theorem :: POLYNOM8:8
for L being non empty ZeroStr, s being AlgSequence of L holds len
s > 0 implies s.(len(s)-1) <> 0.L;
theorem :: POLYNOM8:9
for L being add-associative right_zeroed right_complementable
distributive commutative associative well-unital domRing-like non empty
doubleLoopStr, p,q being Polynomial of L st len p > 0 & len q > 0 holds len(p
*'q) <= len p + len q;
theorem :: POLYNOM8:10
for L being associative non empty doubleLoopStr, k,l being
Element of L, seq being sequence of L holds k * (l * seq) = (k * l) * seq;
begin :: Multiplication of AlgSequences
definition
::$CD
end;
registration
let L be add-associative right_zeroed right_complementable left-distributive
non empty doubleLoopStr;
let m1,m2 be AlgSequence of L;
cluster m1 * m2 -> finite-Support;
end;
theorem :: POLYNOM8:11
for L being add-associative right_zeroed right_complementable
distributive non empty doubleLoopStr, m1,m2 being AlgSequence of L holds len(
m1 * m2) <= min(len m1, len m2);
theorem :: POLYNOM8:12
for L being add-associative right_zeroed right_complementable
distributive domRing-like non empty doubleLoopStr, m1,m2 being AlgSequence of
L st len m1 = len m2 holds len(m1 * m2) = len m1;
begin :: Powers in doubleLoopStrs
definition
let L be associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, a be Element of L;
let i be Integer;
func pow(a,i) -> Element of L equals
:: POLYNOM8:def 3
power(L).(a,i) if 0 <= i
otherwise (power(L).(a,|.i.|))";
end;
theorem :: POLYNOM8:13
for L being associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, x being Element of L holds
pow(x,0) = 1.L;
theorem :: POLYNOM8:14
for L being associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, x being Element of L holds
pow(x,1) = x;
theorem :: POLYNOM8:15
for L being associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, x being Element of L holds
pow(x,-1) = x";
theorem :: POLYNOM8:16
for L being associative commutative well-unital distributive
almost_left_invertible non degenerated non empty doubleLoopStr, i being
Integer holds pow(1.L,i) = 1.L;
theorem :: POLYNOM8:17
for L being associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, x being Element of L, n being
Element of NAT holds pow(x,n+1) = pow(x,n) * x & pow(x,n+1) = x * pow(x,n);
theorem :: POLYNOM8:18
for L being add-associative right_zeroed right_complementable
associative commutative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, i being Integer, x being Element of L st
x <> 0.L holds (pow(x, i))" = pow(x, -i);
theorem :: POLYNOM8:19
for L being Field, j being Integer, x being Element of L st x <>
0.L holds pow(x,j+1) = pow(x,j) * pow(x,1);
theorem :: POLYNOM8:20
for L being Field, j being Integer, x being Element of L st x <>
0.L holds pow(x,j-1) = pow(x,j) * pow(x,-1);
theorem :: POLYNOM8:21
for L being Field, i,j being Integer, x being Element of L st x
<> 0.L holds pow(x,i) * pow(x,j) = pow(x,i+j);
theorem :: POLYNOM8:22
for L being almost_left_invertible associative well-unital
add-associative right_zeroed right_complementable left-distributive commutative
non degenerated non empty doubleLoopStr, k being Element of NAT, x being
Element of L st x <> 0.L holds pow(x", k) = pow(x, -k);
theorem :: POLYNOM8:23
for L being Field, x being Element of L st x <> 0.L 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))
;
theorem :: POLYNOM8:24
for L being associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, x being Element of L, n,m
being Element of NAT holds pow(x, n * m) = pow(pow(x, n), m);
theorem :: POLYNOM8:25
for L being Field, x being Element of L st x <> 0.L for i being
Integer holds pow(x", i) = (pow(x, i))";
theorem :: POLYNOM8:26
for L being Field, x being Element of L st x <> 0.L for i,j
being Integer holds pow(x,i * j) = pow(pow(x,i), j);
theorem :: POLYNOM8:27
for L being associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, x being Element of L, i,k
being Element of NAT st 1 <= k holds pow(x, i*(k-1)) = pow(x|^i, k-1);
begin :: Conversion between AlgSequences and Matrices
definition
let m be Nat, L be non empty ZeroStr, p be AlgSequence of L;
func mConv(p,m) -> Matrix of m,1,L means
:: POLYNOM8:def 4
for i being Nat st 1 <= i & i <= m holds it*(i,1) = p.(i-1);
end;
theorem :: POLYNOM8:28
for m being Nat st m > 0 for L being non empty ZeroStr, 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;
theorem :: POLYNOM8:29
for m being Nat st m > 0 for L being non empty ZeroStr, a being
AlgSequence of L, M being Matrix of m,1,L holds (for i being Nat st i < m holds
M*(i+1,1) = a.i) implies mConv(a,m) = M;
definition
let L be non empty ZeroStr, M be Matrix of L;
func aConv(M) -> AlgSequence of L means
:: 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;
end;
begin :: Primitive Roots, DFT and Vandermonde Matrix
definition
let L be well-unital non empty doubleLoopStr, x be Element of L, 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;
theorem :: POLYNOM8:30
for L being well-unital add-associative right_zeroed
right_complementable right-distributive non degenerated non empty
doubleLoopStr, n being Element of NAT holds not(0.L
is_primitive_root_of_degree n);
theorem :: POLYNOM8:31
for L being add-associative right_zeroed right_complementable
associative commutative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, m being Element of NAT, x being Element
of L st x is_primitive_root_of_degree m holds x" is_primitive_root_of_degree m;
theorem :: POLYNOM8:32
for L being add-associative right_zeroed right_complementable
associative commutative well-unital distributive almost_left_invertible non
degenerated non empty doubleLoopStr, m being Element of NAT, x being Element
of L st x is_primitive_root_of_degree m for i,j being Nat st 1 <= i & i <= m &
1 <= j & j <= m & i <> j holds pow(x,i-j) <> 1.L;
definition
let m be Nat, L be well-unital non empty doubleLoopStr, p be Polynomial of
L, x be Element of L;
func DFT(p,x,m) -> AlgSequence of L means
:: 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;
end;
theorem :: POLYNOM8:33
for m being Nat, L being well-unital non empty doubleLoopStr,
x being Element of L holds DFT(0_.(L),x,m) = 0_.(L);
theorem :: POLYNOM8:34
for m being Nat, L being Field, p,q being Polynomial of L, x
being Element of L holds DFT(p, x, m) * DFT(q, x, m) = DFT(p *' q, x, m);
definition
let L be associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, m be Nat, x be Element of L;
func Vandermonde(x,m) -> Matrix of m,L means
:: 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));
end;
notation
let L be associative commutative well-unital distributive
almost_left_invertible non empty doubleLoopStr, m be Nat, x be Element of L;
synonym VM(x,m) for Vandermonde(x,m);
end;
theorem :: POLYNOM8:35
for L being Field, m,n being Nat st m > 0 for M being Matrix of
m,n,L holds 1.(L,m) * M = M;
theorem :: POLYNOM8:36
for L being Field, m being Element of NAT st 0 < m for u,v,u1
being Matrix of m,L holds (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))) implies u * v = emb(m,L) * u1;
theorem :: POLYNOM8:37
for L being Field, x being Element of L, s being FinSequence of
L, 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;
theorem :: POLYNOM8:38
for L being Field, m,i,j being Element of NAT, 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;
theorem :: POLYNOM8:39
for L being Field, m being Element of NAT st m > 0 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);
theorem :: POLYNOM8:40
for L being Field, m being Element of NAT, 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);
begin :: DFT-Multiplication of Polynomials
theorem :: POLYNOM8:41
for L being Field, p being Polynomial of L, m being Element of
NAT st m > 0 & len p <= m for x being Element of L, i being Element of NAT st i
< m holds DFT(p,x,m).i = VM(x,m) * mConv(p,m)*(i+1,1);
theorem :: POLYNOM8:42
for L being Field, p being Polynomial of L for m being Nat st 0
< m & len p <= m for x being Element of L holds DFT(p,x,m) = aConv(VM(x,m) *
mConv(p, m));
theorem :: POLYNOM8:43
for L being Field, p,q being Polynomial of L, m being Element of
NAT st m > 0 & len p <= m & len q <= m 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);
::$N Multiplication of Polynomials using Discrete Fourier Transformation
theorem :: POLYNOM8:44
for L being Field, p,q being Polynomial of L, m being Element of NAT
st m > 0 & len p <= m & len q <= m for x being Element of L st x
is_primitive_root_of_degree 2*m holds emb(2*m,L) <> 0.L implies (emb(2*m,L))" *
DFT(DFT(p,x,2*m) * DFT(q,x,2*m), x", 2*m) = p *' q;