let L be 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
let p be 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
let m be Element of NAT ; ( m > 0 & len p <= m implies 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 )
assume that
A1:
m > 0
and
A2:
len p <= m
; 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
let x be 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
set v = VM x,m;
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
A3:
for
k being
Nat st
k < m holds
(Col (mConv p,m),1) . (k + 1) = p . k
proof
let k be
Nat;
( k < m implies (Col (mConv p,m),1) . (k + 1) = p . k )
assume A4:
k < m
;
(Col (mConv p,m),1) . (k + 1) = p . k
then
( 1
<= k + 1 &
k + 1
<= m )
by NAT_1:11, NAT_1:13;
then A5:
k + 1
in Seg m
;
len (mConv p,m) = m
by A1, Th28;
then
k + 1
in dom (mConv p,m)
by A5, FINSEQ_1:def 3;
then
(Col (mConv p,m),1) . (k + 1) = (mConv p,m) * (k + 1),1
by MATRIX_1:def 9;
hence
(Col (mConv p,m),1) . (k + 1) = p . k
by A4, Th28;
verum
end;
A6:
width (VM x,m) =
m
by MATRIX_1:25
.=
len (mConv p,m)
by A1, Th28
;
then A7:
len ((VM x,m) * (mConv p,m)) =
len (VM x,m)
by MATRIX_3:def 4
.=
m
by MATRIX_1:25
;
width ((VM x,m) * (mConv p,m)) =
width (mConv p,m)
by A6, MATRIX_3:def 4
.=
1
by A1, Th28
;
then
(VM x,m) * (mConv p,m) is
Matrix of
m,1,
L
by A1, A7, MATRIX_1:20;
then A8:
Indices ((VM x,m) * (mConv p,m)) = [:(Seg m),(Seg (width ((VM x,m) * (mConv p,m)))):]
by MATRIX_1:26;
A9:
len (mConv p,m) =
m
by A1, Th28
.=
width (VM x,m)
by MATRIX_1:25
;
width ((VM x,m) * (mConv p,m)) =
width (mConv p,m)
by A6, MATRIX_3:def 4
.=
1
by A1, Th28
;
then A10:
1
in Seg (width ((VM x,m) * (mConv p,m)))
;
let i be
Element of
NAT ;
( i < m implies (DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1 )
assume A11:
i < m
;
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
A12:
for
k being
Nat st
k < m holds
(Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),
(k + 1)
proof
let k be
Nat;
( k < m implies (Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),(k + 1) )
assume
k < m
;
(Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),(k + 1)
then
( 1
<= k + 1 &
k + 1
<= m )
by NAT_1:11, NAT_1:13;
then
k + 1
in Seg m
;
then
k + 1
in Seg (width (VM x,m))
by MATRIX_1:25;
hence
(Line (VM x,m),(i + 1)) . (k + 1) = (VM x,m) * (i + 1),
(k + 1)
by MATRIX_1:def 8;
verum
end;
A13:
for
k being
Nat st
k < m holds
(Line (VM x,m),(i + 1)) . (k + 1) = pow x,
(i * k)
proof
let k be
Nat;
( k < m implies (Line (VM x,m),(i + 1)) . (k + 1) = pow x,(i * k) )
assume A14:
k < m
;
(Line (VM x,m),(i + 1)) . (k + 1) = pow x,(i * k)
then A15:
( 1
<= k + 1 &
k + 1
<= m )
by NAT_1:11, NAT_1:13;
A16:
( 1
<= i + 1 &
i + 1
<= m )
by A11, NAT_1:11, NAT_1:13;
(Line (VM x,m),(i + 1)) . (k + 1) =
(VM x,m) * (i + 1),
(k + 1)
by A12, A14
.=
pow x,
(((i + 1) - 1) * ((k + 1) - 1))
by A16, A15, Def8
.=
pow x,
(i * k)
;
hence
(Line (VM x,m),(i + 1)) . (k + 1) = pow x,
(i * k)
;
verum
end;
A17:
for
k being
Nat for
a,
b,
c being
Element of
L st
a = (Line (VM x,m),(i + 1)) . (k + 1) &
b = (Col (mConv p,m),1) . (k + 1) &
c = p . k &
k < m holds
a * b = (pow x,(i * k)) * c
proof
let k be
Nat;
for a, b, c being Element of L st a = (Line (VM x,m),(i + 1)) . (k + 1) & b = (Col (mConv p,m),1) . (k + 1) & c = p . k & k < m holds
a * b = (pow x,(i * k)) * clet a,
b,
c be
Element of
L;
( a = (Line (VM x,m),(i + 1)) . (k + 1) & b = (Col (mConv p,m),1) . (k + 1) & c = p . k & k < m implies a * b = (pow x,(i * k)) * c )
assume that A18:
a = (Line (VM x,m),(i + 1)) . (k + 1)
and A19:
(
b = (Col (mConv p,m),1) . (k + 1) &
c = p . k )
and A20:
k < m
;
a * b = (pow x,(i * k)) * c
a = pow x,
(i * k)
by A13, A18, A20;
hence
a * b = (pow x,(i * k)) * c
by A3, A19, A20;
verum
end;
A21:
for
k being
Element of
NAT st 1
<= k &
k <= m holds
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))
proof
A22:
len (mConv p,m) = m
by A1, Th28;
let k be
Element of
NAT ;
( 1 <= k & k <= m implies (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1)) )
assume that A23:
1
<= k
and A24:
k <= m
;
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))
k in Seg m
by A23, A24;
then
k in dom (mConv p,m)
by A22, FINSEQ_1:def 3;
then A25:
(Col (mConv p,m),1) . k = (mConv p,m) * k,1
by MATRIX_1:def 9;
0 < k
by A23;
then
(
dom p = NAT &
k - 1 is
Element of
NAT )
by FUNCT_2:def 1, NAT_1:20;
then A26:
p . (k - 1) = p /. (k - 1)
by PARTFUN1:def 8;
Seg (width (VM x,m)) = Seg m
by MATRIX_1:25;
then
k in Seg (width (VM x,m))
by A23, A24;
then
(Line (VM x,m),(i + 1)) . k = (VM x,m) * (i + 1),
k
by MATRIX_1:def 8;
then reconsider a =
(Line (VM x,m),(i + 1)) . k,
b =
(Col (mConv p,m),1) . k,
c =
p . (k - 1) as
Element of
L by A25, A26;
len (Line (VM x,m),(i + 1)) =
width (VM x,m)
by MATRIX_1:def 8
.=
m
by MATRIX_1:25
.=
len (mConv p,m)
by A1, Th28
.=
len (Col (mConv p,m),1)
by MATRIX_1:def 9
;
then len (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) =
len (Line (VM x,m),(i + 1))
by MATRIX_3:8
.=
width (VM x,m)
by MATRIX_1:def 8
.=
m
by MATRIX_1:25
;
then
dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = Seg m
by FINSEQ_1:def 3;
then
k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1))
by A23, A24;
then A27:
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = a * b
by FVSUM_1:73;
A28:
a * b = (pow x,(i * (k - 1))) * c
reconsider d =
pow x,
(i * (k - 1)) as
Element of
L ;
A32:
k - 1
>= 0
by A23, NAT_1:20;
d =
pow (x |^ i),
(k - 1)
by A23, Th27
.=
(power L) . (x |^ i),
(k - 1)
by A32, Def3
.=
(power L) . (x |^ i),
(k -' 1)
by A32, XREAL_0:def 2
;
hence
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))
by A28, A27, A32, XREAL_0:def 2;
verum
end;
A33:
Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = eval p,
(x |^ i)
proof
A34:
for
k being
Nat st
len p < k &
k <= m holds
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L
proof
A35:
1
<= 1
+ (len p)
by NAT_1:11;
let k be
Nat;
( len p < k & k <= m implies (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L )
assume that A36:
len p < k
and A37:
k <= m
;
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L
A38:
len p < (k - 1) + 1
by A36;
(len p) + 1
<= k
by A36, NAT_1:13;
then A39:
1
<= k
by A35, XXREAL_0:2;
then
1
- 1
<= k - 1
by XREAL_1:11;
then
k -' 1
= k - 1
by XREAL_0:def 2;
then A40:
k -' 1
>= len p
by A38, NAT_1:13;
k in NAT
by ORDINAL1:def 13;
then (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k =
(p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))
by A21, A37, A39
.=
(0. L) * ((power L) . (x |^ i),(k -' 1))
by A40, ALGSEQ_1:22
.=
0. L
by VECTSP_1:39
;
hence
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = 0. L
;
verum
end;
len (Line (VM x,m),(i + 1)) =
width (VM x,m)
by MATRIX_1:def 8
.=
m
by MATRIX_1:25
.=
len (mConv p,m)
by A1, Th28
.=
len (Col (mConv p,m),1)
by MATRIX_1:def 9
;
then A41:
len (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) =
len (Line (VM x,m),(i + 1))
by MATRIX_3:8
.=
width (VM x,m)
by MATRIX_1:def 8
.=
m
by MATRIX_1:25
;
(len p) - (len p) <= m - (len p)
by A2, XREAL_1:11;
then reconsider lengthG =
m - (len p) as
Element of
NAT by INT_1:16;
consider F being
FinSequence of
L such that A42:
eval p,
(x |^ i) = Sum F
and A43:
len F = len p
and A44:
for
k being
Element of
NAT st
k in dom F holds
F . k = (p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))
by POLYNOM4:def 2;
ex
G being
FinSequence of
L st
(
dom G = Seg lengthG & ( for
k being
Nat st
k in Seg lengthG holds
G . k = 0. L ) )
then consider G being
FinSequence of
L such that A46:
dom G = Seg lengthG
and A47:
for
k being
Nat st
k in Seg lengthG holds
G . k = 0. L
;
A48:
for
k being
Element of
NAT st
k in Seg lengthG holds
G . k = 0. L
by A47;
A49:
len G = m - (len p)
by A46, FINSEQ_1:def 3;
then
(len F) + (len G) = m
by A43;
then
dom (F ^ G) = Seg m
by FINSEQ_1:def 7;
then A50:
dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = dom (F ^ G)
by A41, FINSEQ_1:def 3;
A51:
for
k being
Element of
NAT st 1
<= k &
k <= len p holds
F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k
proof
let k be
Element of
NAT ;
( 1 <= k & k <= len p implies F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k )
assume that A52:
1
<= k
and A53:
k <= len p
;
F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k
A54:
k <= m
by A2, A53, XXREAL_0:2;
dom F = Seg (len p)
by A43, FINSEQ_1:def 3;
then
k in dom F
by A52, A53;
then F . k =
(p . (k -' 1)) * ((power L) . (x |^ i),(k -' 1))
by A44
.=
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k
by A21, A52, A54
;
hence
F . k = (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k
;
verum
end;
for
k being
Nat st
k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) holds
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k
proof
let k be
Nat;
( k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) implies (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k )
(len F) + (len G) = m
by A43, A49;
then A55:
dom (F ^ G) = Seg m
by FINSEQ_1:def 7;
assume A56:
k in dom (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1))
;
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k
per cases
( ( 1 <= k & k <= len F ) or ( len F < k & k <= m ) )
by A50, A56, A55, FINSEQ_1:3;
suppose A57:
( 1
<= k &
k <= len F )
;
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . kthen
k in dom F
by FINSEQ_3:27;
then (F ^ G) . k =
F . k
by FINSEQ_1:def 7
.=
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k
by A43, A51, A56, A57
;
hence
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k
;
verum end; suppose A58:
(
len F < k &
k <= m )
;
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . kthen
(len F) + 1
<= k
by NAT_1:13;
then
((len F) + 1) - (len F) <= k - (len F)
by XREAL_1:11;
then reconsider l =
k - (len F) as
Element of
NAT by INT_1:16;
(len p) - m <= m - m
by A2, XREAL_1:11;
then
- ((len p) - m) >= 0
;
then reconsider lengthG =
m - (len p) as
Element of
NAT by INT_1:16;
(len F) + 1
<= k
by A58, NAT_1:13;
then A59:
((len F) + 1) - (len F) <= k - (len F)
by XREAL_1:11;
l <= lengthG
by A43, A58, XREAL_1:11;
then A60:
l in dom G
by A46, A59;
(len F) + (len G) = m
by A43, A49;
then
dom (F ^ G) = Seg m
by FINSEQ_1:def 7;
then
len (F ^ G) = m
by FINSEQ_1:def 3;
then (F ^ G) . k =
G . (k - (len F))
by A58, FINSEQ_1:37
.=
0. L
by A46, A47, A60
.=
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k
by A43, A34, A58
;
hence
(mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) . k = (F ^ G) . k
;
verum end;
end;
then
mlt (Line (VM x,m),(i + 1)),
(Col (mConv p,m),1) = F ^ G
by A50, FINSEQ_1:17;
then Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) =
(Sum F) + (Sum G)
by RLVECT_1:58
.=
(Sum F) + (0. L)
by A46, A48, POLYNOM3:1
.=
eval p,
(x |^ i)
by A42, RLVECT_1:def 7
;
hence
Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1)) = eval p,
(x |^ i)
;
verum
end;
A61:
(Line (VM x,m),(i + 1)) "*" (Col (mConv p,m),1) = Sum (mlt (Line (VM x,m),(i + 1)),(Col (mConv p,m),1))
by FVSUM_1:def 10;
( 1
<= i + 1 &
i + 1
<= m )
by A11, NAT_1:11, NAT_1:13;
then
i + 1
in Seg m
;
then
[(i + 1),1] in Indices ((VM x,m) * (mConv p,m))
by A8, A10, ZFMISC_1:def 2;
then
((VM x,m) * (mConv p,m)) * (i + 1),1
= eval p,
(x |^ i)
by A9, A61, A33, MATRIX_3:def 4;
hence
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
by A11, Def7;
verum
end;
hence
for i being Element of NAT st i < m holds
(DFT p,x,m) . i = ((VM x,m) * (mConv p,m)) * (i + 1),1
; verum