:: Multiplication of Polynomials using {D}iscrete {F}ourier {T}ransformation
::  by Krzysztof Treyderowski and Christoph Schwarzweller
::
:: Received October 12, 2006
:: Copyright (c) 2006-2021 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;