:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation :: by Krzysztof Treyderowski and Christoph Schwarzweller :: :: Received October 12, 2006 :: Copyright (c) 2006-2012 Association of Mizar Users begin Lm1: for j being Integer holds ( j >= 0 or j = - 1 or j < - 1 ) proofend; Lm2: for j being Integer holds ( j >= 1 or j = 0 or j < 0 ) proofend; theorem Th1: :: POLYNOM8:1 for n being Element of 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 proofend; registration cluster non empty right_complementable almost_left_invertible associative right-distributive well-unital add-associative right_zeroed -> non empty right_complementable associative right-distributive well-unital add-associative right_zeroed domRing-like for doubleLoopStr ; coherence for b1 being non empty right_complementable associative right-distributive well-unital add-associative right_zeroed doubleLoopStr st b1 is almost_left_invertible holds b1 is domRing-like proofend; end; theorem Th2: :: POLYNOM8:2 for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for x, y being Element of L st x <> 0. L & y <> 0. L holds (x * y) " = (x ") * (y ") proofend; theorem Th3: :: POLYNOM8:3 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for z, z1 being Element of L st z <> 0. L holds z1 = (z1 * z) / z proofend; 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) proofend; theorem Th5: :: POLYNOM8:5 for L being non empty right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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) proofend; 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) proofend; 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 proofend; 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 proofend; theorem Th9: :: POLYNOM8:9 for L being non empty right_complementable associative commutative well-unital distributive add-associative right_zeroed 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) proofend; 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 proofend; begin definition let L be non empty doubleLoopStr ; let m1, m2 be sequence of L; funcm1 * m2 -> sequence of L means :Def2: :: POLYNOM8:def 2 for i being Nat holds it . i = (m1 . i) * (m2 . i); existence ex b1 being sequence of L st for i being Nat holds b1 . i = (m1 . i) * (m2 . i) proofend; uniqueness for b1, b2 being sequence of L st ( for i being Nat holds b1 . i = (m1 . i) * (m2 . i) ) & ( for i being Nat holds b2 . i = (m1 . i) * (m2 . i) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines * POLYNOM8:def_2_:_ for L being non empty doubleLoopStr for m1, m2, b4 being sequence of L holds ( b4 = m1 * m2 iff for i being Nat holds b4 . i = (m1 . i) * (m2 . i) ); registration let L be non empty right_complementable left-distributive add-associative right_zeroed doubleLoopStr ; let m1, m2 be AlgSequence of L; clusterm1 * m2 -> finite-Support ; coherence m1 * m2 is finite-Support proofend; 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)) proofend; 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 proofend; begin definition let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; let a be Element of L; let i be Integer; func pow (a,i) -> Element of L equals :Def3: :: POLYNOM8:def 3 (power L) . (a,i) if 0 <= i otherwise ((power L) . (a,(abs i))) " ; coherence ( ( 0 <= i implies (power L) . (a,i) is Element of L ) & ( not 0 <= i implies ((power L) . (a,(abs i))) " is Element of L ) ) proofend; consistency for b1 being Element of L holds verum ; end; :: deftheorem Def3 defines pow POLYNOM8:def_3_:_ for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for a being Element of L for i being Integer holds ( ( 0 <= i implies pow (a,i) = (power L) . (a,i) ) & ( not 0 <= i implies pow (a,i) = ((power L) . (a,(abs i))) " ) ); theorem Th13: :: POLYNOM8:13 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L holds pow (x,0) = 1. L proofend; Lm3: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for a being Element of L for i being Integer st 0 > i holds pow (a,i) = (pow (a,(abs i))) " proofend; Lm4: for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr for i being Integer for x being Element of L st i <= 0 holds pow (x,i) = (pow (x,(abs i))) " proofend; theorem Th14: :: POLYNOM8:14 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L holds pow (x,1) = x proofend; theorem Th15: :: POLYNOM8:15 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L holds pow (x,(- 1)) = x " proofend; Lm5: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for i being Element of NAT holds pow ((1. L),i) = 1. L proofend; theorem Th16: :: POLYNOM8:16 for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive doubleLoopStr for i being Integer holds pow ((1. L),i) = 1. L proofend; theorem Th17: :: POLYNOM8:17 for L being non empty almost_left_invertible associative commutative well-unital distributive 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)) ) proofend; Lm6: for L being non empty well-unital doubleLoopStr for n being Element of NAT holds (1. L) |^ n = 1. L proofend; Lm7: for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for m being Element of NAT for x being Element of L st x <> 0. L holds (x |^ m) * ((x ") |^ m) = 1. L proofend; theorem Th18: :: POLYNOM8:18 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for i being Integer for x being Element of L st x <> 0. L holds (pow (x,i)) " = pow (x,(- i)) proofend; 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)) proofend; 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))) proofend; 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)) proofend; Lm8: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr for k being Element of NAT for x being Element of L st x <> 0. L holds (x ") |^ k = (x |^ k) " proofend; theorem Th22: :: POLYNOM8:22 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative left-distributive well-unital add-associative right_zeroed doubleLoopStr for k being Element of NAT for x being Element of L st x <> 0. L holds pow ((x "),k) = pow (x,(- k)) proofend; 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))) proofend; theorem Th24: :: POLYNOM8:24 for L being non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr for x being Element of L for n, m being Element of NAT holds pow (x,(n * m)) = pow ((pow (x,n)),m) proofend; Lm9: for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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)) " proofend; 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)) " proofend; 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) proofend; theorem Th27: :: POLYNOM8:27 for L being non empty almost_left_invertible associative commutative well-unital distributive 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)) proofend; Lm10: for L being non empty almost_left_invertible associative commutative well-unital distributive 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 proofend; Lm11: for L being non empty non degenerated almost_left_invertible associative commutative well-unital distributive 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 proofend; begin 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 :Def4: :: 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) proofend; 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 proofend; end; :: deftheorem Def4 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 ) ) proofend; 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 proofend; definition let L be non empty ZeroStr ; let M be Matrix of L; func aConv M -> AlgSequence of L means :Def5: :: 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 ) ) proofend; 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 proofend; end; :: deftheorem Def5 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 ) ) ); begin definition let L be non empty well-unital doubleLoopStr ; let x be Element of L; let n be Element of NAT ; predx is_primitive_root_of_degree n means :Def6: :: 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 Def6 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 proofend; theorem Th31: :: POLYNOM8:31 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed doubleLoopStr for m being Element of NAT for x being Element of L st x is_primitive_root_of_degree m holds x " is_primitive_root_of_degree m proofend; theorem Th32: :: POLYNOM8:32 for L being non empty non degenerated right_complementable almost_left_invertible associative commutative well-unital distributive add-associative right_zeroed 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 proofend; 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 :Def7: :: 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 ) ) proofend; 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 proofend; end; :: deftheorem Def7 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 proofend; 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) proofend; definition let L be non empty almost_left_invertible associative commutative well-unital distributive doubleLoopStr ; let m be Nat; let x be Element of L; func Vandermonde (x,m) -> Matrix of m,L means :Def8: :: 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))) proofend; 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 proofend; end; :: deftheorem Def8 defines Vandermonde POLYNOM8:def_8_:_ for L being non empty almost_left_invertible associative commutative well-unital distributive 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 associative commutative well-unital distributive 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 proofend; 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 proofend; 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))) proofend; 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 proofend; 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 proofend; 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)) proofend; 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)) proofend; begin 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) proofend; 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))) proofend; 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) proofend; :: [WP: ] 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 proofend;