Definition df-vts 33934

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 33933	. 2 class vts
2		vl	. . 3 setvar 𝑙
3		vn	. . 3 setvar 𝑛
4		cc 11110	. . . 4 class ℂ
5		cn 12216	. . . 4 class ℕ
6		cmap 8822	. . . 4 class ↑m
7	4, 5, 6	co 7411	. . 3 class (ℂ ↑m ℕ)
8		cn0 12476	. . 3 class ℕ0
9		vx	. . . 4 setvar 𝑥
10		c1 11113	. . . . . 6 class 1
11	3	cv 1540	. . . . . 6 class 𝑛
12		cfz 13488	. . . . . 6 class ...
13	10, 11, 12	co 7411	. . . . 5 class (1...𝑛)
14		va	. . . . . . . 8 setvar 𝑎
15	14	cv 1540	. . . . . . 7 class 𝑎
16	2	cv 1540	. . . . . . 7 class 𝑙
17	15, 16	cfv 6543	. . . . . 6 class (𝑙‘𝑎)
18		ci 11114	. . . . . . . . 9 class i
19		c2 12271	. . . . . . . . . 10 class 2
20		cpi 16014	. . . . . . . . . 10 class π
21		cmul 11117	. . . . . . . . . 10 class ·
22	19, 20, 21	co 7411	. . . . . . . . 9 class (2 · π)
23	18, 22, 21	co 7411	. . . . . . . 8 class (i · (2 · π))
24	9	cv 1540	. . . . . . . . 9 class 𝑥
25	15, 24, 21	co 7411	. . . . . . . 8 class (𝑎 · 𝑥)
26	23, 25, 21	co 7411	. . . . . . 7 class ((i · (2 · π)) · (𝑎 · 𝑥))
27		ce 16009	. . . . . . 7 class exp
28	26, 27	cfv 6543	. . . . . 6 class (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))
29	17, 28, 21	co 7411	. . . . 5 class ((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))
30	13, 29, 14	csu 15636	. . . 4 class Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))
31	9, 4, 30	cmpt 5231	. . 3 class (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))))
32	2, 3, 7, 8, 31	cmpo 7413	. 2 class (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
33	1, 32	wceq 1541	1 wff vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙‘𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))

This definition is referenced by:  vtsval  33935