Definition df-vts

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

	Ref	Expression
Assertion	df-vts	$$⊢\mathrm{vts}=\left(l\in \left({ℂ}^{\mathbb{N}}\right),n\in {\mathbb{N}}_0⟼\left(x\in ℂ⟼\sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvts	$$class\mathrm{vts}$$
1		vl	$$setvarl$$
2		cc	$$classℂ$$
3		cmap	$$class{\uparrow }_{𝑚}$$
4		cn	$$class\mathbb{N}$$
5	2 4 3	co	$$class\left({ℂ}^{\mathbb{N}}\right)$$
6		vn	$$setvarn$$
7		cn0	$$class{\mathbb{N}}_0$$
8		vx	$$setvarx$$
9		va	$$setvara$$
10		c1	$$class1$$
11		cfz	$$class\dots$$
12	6	cv	$$setvarn$$
13	10 12 11	co	$$class\left(1\dots n\right)$$
14	1	cv	$$setvarl$$
15	9	cv	$$setvara$$
16	15 14	cfv	$$classl\left(a\right)$$
17		cmul	$$class\times$$
18		ce	$$class\exp$$
19		ci	$$class\mathrm{i}$$
20		c2	$$class2$$
21		cpi	$$class\mathrm{\pi }$$
22	20 21 17	co	$$class2\mathrm{\pi }$$
23	19 22 17	co	$$class\mathrm{i}2\mathrm{\pi }$$
24	8	cv	$$setvarx$$
25	15 24 17	co	$$classax$$
26	23 25 17	co	$$class\mathrm{i}2\mathrm{\pi }ax$$
27	26 18	cfv	$$class{\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}$$
28	16 27 17	co	$$classl\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}$$
29	13 28 9	csu	$$class\sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}$$
30	8 2 29	cmpt	$$class\left(x\in ℂ⟼\sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)$$
31	1 6 5 7 30	cmpo	$$class\left(l\in \left({ℂ}^{\mathbb{N}}\right),n\in {\mathbb{N}}_0⟼\left(x\in ℂ⟼\sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)\right)$$
32	0 31	wceq	$$wff\mathrm{vts}=\left(l\in \left({ℂ}^{\mathbb{N}}\right),n\in {\mathbb{N}}_0⟼\left(x\in ℂ⟼\sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)\right)$$