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_0:def 8;
hence
(Col ((mConv (p,m)),1)) . (k + 1) = p . k
by A4, Th28;
verum
end;
A6:
width (VM (x,m)) =
m
by MATRIX_0:24
.=
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_0:24
;
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_0:20;
then A8:
Indices ((VM (x,m)) * (mConv (p,m))) = [:(Seg m),(Seg (width ((VM (x,m)) * (mConv (p,m))))):]
by MATRIX_0:25;
A9:
len (mConv (p,m)) =
m
by A1, Th28
.=
width (VM (x,m))
by MATRIX_0:24
;
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_0:24;
hence
(Line ((VM (x,m)),(i + 1))) . (k + 1) = (VM (x,m)) * (
(i + 1),
(k + 1))
by MATRIX_0:def 7;
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, Def7
.=
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_0:def 8;
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 6;
Seg (width (VM (x,m))) = Seg m
by MATRIX_0:24;
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_0:def 7;
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_0:def 7
.=
m
by MATRIX_0:24
.=
len (mConv (p,m))
by A1, Th28
.=
len (Col ((mConv (p,m)),1))
by MATRIX_0:def 8
;
then len (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) =
len (Line ((VM (x,m)),(i + 1)))
by MATRIX_3:6
.=
width (VM (x,m))
by MATRIX_0:def 7
.=
m
by MATRIX_0:24
;
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:60;
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, Def2
.=
(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:9;
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 12;
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:8
.=
0. L
;
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_0:def 7
.=
m
by MATRIX_0:24
.=
len (mConv (p,m))
by A1, Th28
.=
len (Col ((mConv (p,m)),1))
by MATRIX_0:def 8
;
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:6
.=
width (VM (x,m))
by MATRIX_0:def 7
.=
m
by MATRIX_0:24
;
(len p) - (len p) <= m - (len p)
by A2, XREAL_1:9;
then reconsider lengthG =
m - (len p) as
Element of
NAT by INT_1:3;
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:1;
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:25;
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:9;
then reconsider l =
k - (len F) as
Element of
NAT by INT_1:3;
(len p) - m <= m - m
by A2, XREAL_1:9;
then
- ((len p) - m) >= 0
;
then reconsider lengthG =
m - (len p) as
Element of
NAT by INT_1:3;
(len F) + 1
<= k
by A58, NAT_1:13;
then A59:
((len F) + 1) - (len F) <= k - (len F)
by XREAL_1:9;
l <= lengthG
by A43, A58, XREAL_1:9;
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:24
.=
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;
end;
then
mlt (
(Line ((VM (x,m)),(i + 1))),
(Col ((mConv (p,m)),1)))
= F ^ G
by A50, FINSEQ_1:13;
then Sum (mlt ((Line ((VM (x,m)),(i + 1))),(Col ((mConv (p,m)),1)))) =
(Sum F) + (Sum G)
by RLVECT_1:41
.=
(Sum F) + (0. L)
by A46, A48, POLYNOM3:1
.=
eval (
p,
(x |^ i))
by A42, RLVECT_1:def 4
;
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 9;
( 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, Def6;
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