Definition df-vts 35318

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

Assertion

Ref	Expression
df-vts	⊢ vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))

Distinct variable group:   𝑎,𝑙,𝑛,𝑥

Detailed syntax breakdown of Definition df-vts

Step	Hyp	Ref	Expression
1		cvts 35317	. 2 class vts
2		vl	. . 3 setvar 𝑙
3		vn	. . 3 setvar 𝑛
4		cc 11208	. . . 4 class ℂ
5		cn 12345	. . . 4 class ℕ
6		cmap 8858	. . . 4 class ↑m
7	4, 5, 6	co 7427	. . 3 class (ℂ ↑m ℕ)
8		cn0 12616	. . 3 class ℕ0
9		vx	. . . 4 setvar 𝑥
10		c1 11211	. . . . . 6 class 1
11	3	cv 1568	. . . . . 6 class 𝑛
12		cfz 13649	. . . . . 6 class ...
13	10, 11, 12	co 7427	. . . . 5 class (1...𝑛)
14		va	. . . . . . . 8 setvar 𝑎
15	14	cv 1568	. . . . . . 7 class 𝑎
16	2	cv 1568	. . . . . . 7 class 𝑙
17	15, 16	cfv 6546	. . . . . 6 class (𝑙‘𝑎)
18		ci 11212	. . . . . . . . 9 class i
19		c2 12407	. . . . . . . . . 10 class 2
20		cpi 16244	. . . . . . . . . 10 class π
21		cmul 11215	. . . . . . . . . 10 class ·
22	19, 20, 21	co 7427	. . . . . . . . 9 class (2 · π)
23	18, 22, 21	co 7427	. . . . . . . 8 class (i · (2 · π))
24	9	cv 1568	. . . . . . . . 9 class 𝑥
25	15, 24, 21	co 7427	. . . . . . . 8 class (𝑎 · 𝑥)
26	23, 25, 21	co 7427	. . . . . . 7 class ((i · (2 · π)) · (𝑎 · 𝑥))
27		ce 16239	. . . . . . 7 class exp
28	26, 27	cfv 6546	. . . . . 6 class (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))
29	17, 28, 21	co 7427	. . . . 5 class ((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))
30	13, 29, 14	csu 15865	. . . 4 class Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))
31	9, 4, 30	cmpt 5188	. . 3 class (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))))
32	2, 3, 7, 8, 31	cmpo 7429	. 2 class (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
33	1, 32	wceq 1569	1 wff vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))

This definition is used by:  vtsval  35319