let L be 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)))
let p be 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)))
let m be Nat; ( 0 < m & len p <= m implies for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m))) )
assume that
A1:
0 < m
and
A2:
len p <= m
; for x being Element of L holds DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
let x be Element of L; DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
A3:
m in NAT
by ORDINAL1:def 12;
A4:
now for u9 being object st u9 in dom (DFT (p,x,m)) holds
(DFT (p,x,m)) . u9 = (aConv ((VM (x,m)) * (mConv (p,m)))) . u9let u9 be
object ;
( u9 in dom (DFT (p,x,m)) implies (DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 )assume
u9 in dom (DFT (p,x,m))
;
(DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1then reconsider u =
u9 as
Element of
NAT by FUNCT_2:def 1;
per cases
( u < m or m <= u )
;
suppose A5:
u < m
;
(DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 width (VM (x,m)) =
m
by MATRIX_0:24
.=
len (mConv (p,m))
by A1, Th28
;
then A6:
len ((VM (x,m)) * (mConv (p,m))) =
len (VM (x,m))
by MATRIX_3:def 4
.=
m
by MATRIX_0:24
;
thus (DFT (p,x,m)) . u9 =
((VM (x,m)) * (mConv (p,m))) * (
(u + 1),1)
by A3, A2, A5, Th41
.=
(aConv ((VM (x,m)) * (mConv (p,m)))) . u9
by A5, A6, Def4
;
verum end; suppose A7:
m <= u
;
(DFT (p,x,m)) . b1 = (aConv ((VM (x,m)) * (mConv (p,m)))) . b1 width (VM (x,m)) =
m
by MATRIX_0:24
.=
len (mConv (p,m))
by A1, Th28
;
then A8:
len ((VM (x,m)) * (mConv (p,m))) =
len (VM (x,m))
by MATRIX_3:def 4
.=
m
by MATRIX_0:24
;
thus (DFT (p,x,m)) . u9 =
0. L
by A7, Def6
.=
(aConv ((VM (x,m)) * (mConv (p,m)))) . u9
by A7, A8, Def4
;
verum end; end; end;
dom (DFT (p,x,m)) =
NAT
by FUNCT_2:def 1
.=
dom (aConv ((VM (x,m)) * (mConv (p,m))))
by FUNCT_2:def 1
;
hence
DFT (p,x,m) = aConv ((VM (x,m)) * (mConv (p,m)))
by A4, FUNCT_1:2; verum