Definition df-vts 30714

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

Assertion

Ref	Expression
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 ) ) ) ) ) )

Distinct variable group:   a, l, n, x

Detailed syntax breakdown of Definition df-vts

Step	Hyp	Ref	Expression
1		cvts 30713	. 2 class vts
2		vl	. . 3 setvar l
3		vn	. . 3 setvar n
4		cc 9934	. . . 4 class CC
5		cn 11020	. . . 4 class NN
6		cmap 7857	. . . 4 class ^m
7	4, 5, 6	co 6650	. . 3 class ( CC ^m NN )
8		cn0 11292	. . 3 class NN0
9		vx	. . . 4 setvar x
10		c1 9937	. . . . . 6 class 1
11	3	cv 1482	. . . . . 6 class n
12		cfz 12326	. . . . . 6 class ...
13	10, 11, 12	co 6650	. . . . 5 class ( 1 ... n )
14		va	. . . . . . . 8 setvar a
15	14	cv 1482	. . . . . . 7 class a
16	2	cv 1482	. . . . . . 7 class l
17	15, 16	cfv 5888	. . . . . 6 class ( l ` a )
18		ci 9938	. . . . . . . . 9 class _i
19		c2 11070	. . . . . . . . . 10 class 2
20		cpi 14797	. . . . . . . . . 10 class pi
21		cmul 9941	. . . . . . . . . 10 class x.
22	19, 20, 21	co 6650	. . . . . . . . 9 class ( 2 x. pi )
23	18, 22, 21	co 6650	. . . . . . . 8 class ( _i x. ( 2 x. pi ) )
24	9	cv 1482	. . . . . . . . 9 class x
25	15, 24, 21	co 6650	. . . . . . . 8 class ( a x. x )
26	23, 25, 21	co 6650	. . . . . . 7 class ( ( _i x. ( 2 x. pi ) ) x. ( a x. x ) )
27		ce 14792	. . . . . . 7 class exp
28	26, 27	cfv 5888	. . . . . 6 class ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( a x. x ) ) )
29	17, 28, 21	co 6650	. . . . 5 class ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( a x. x ) ) ) )
30	13, 29, 14	csu 14416	. . . 4 class sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( a x. x ) ) ) )
31	9, 4, 30	cmpt 4729	. . 3 class ( x e. CC |-> sum_ a e. ( 1 ... n ) ( ( l ` a ) x. ( exp ` ( ( _i x. ( 2 x. pi ) ) x. ( a x. x ) ) ) ) )
32	2, 3, 7, 8, 31	cmpt2 6652	. 2 class ( 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 ) ) ) ) ) )
33	1, 32	wceq 1483	1 wff 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 ) ) ) ) ) )

This definition is referenced by:  vtsval  30715