Metamath Proof Explorer

Definition df-vts

Description: Define the Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 1-Dec-2021)

Ref Expression
Assertion df-vts 
|- vts = ( l e. ( CC ^m NN ) , n e. NN0 |-> ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvts 
 |-  vts
1 vl 
 |-  l
2 cc 
 |-  CC
3 cmap 
 |-  ^m
4 cn 
 |-  NN
5 2 4 3 co 
 |-  ( CC ^m NN )
6 vn 
 |-  n
7 cn0 
 |-  NN0
8 vx 
 |-  x
9 va 
 |-  a
10 c1 
 |-  1
11 cfz 
 |-  ...
12 6 cv 
 |-  n
13 10 12 11 co 
 |-  ( 1 ... n )
14 1 cv 
 |-  l
15 9 cv 
 |-  a
16 15 14 cfv 
 |-  ( l ` a )
17 cmul 
 |-  x.
18 ce 
 |-  exp
19 ci 
 |-  _i
20 c2 
 |-  2
21 cpi 
 |-  _pi
22 20 21 17 co 
 |-  ( 2 x. _pi )
23 19 22 17 co 
 |-  ( _i x. ( 2 x. _pi ) )
24 8 cv 
 |-  x
25 15 24 17 co 
 |-  ( a x. x )
26 23 25 17 co 
 |-  ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) )
27 26 18 cfv 
 |-  ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) )
28 16 27 17 co 
 |-  ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) )
29 13 28 9 csu 
 |-  sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) )
30 8 2 29 cmpt 
 |-  ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) )
31 1 6 5 7 30 cmpo 
 |-  ( l e. ( CC ^m NN ) , n e. NN0 |-> ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )
32 0 31 wceq 
 |-  vts = ( l e. ( CC ^m NN ) , n e. NN0 |-> ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( a x. x ) ) ) ) ) )