df-vts

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

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

Step	Hyp	Ref	Expression
0		cvts	⊢ vts
1		vl	⊢ 𝑙
2		cc	⊢ ℂ
3		cmap	⊢ ↑_m
4		cn	⊢ ℕ
5	2 4 3	co	⊢ ( ℂ ↑_m ℕ )
6		vn	⊢ 𝑛
7		cn0	⊢ ℕ₀
8		vx	⊢ 𝑥
9		va	⊢ 𝑎
10		c1	⊢ 1
11		cfz	⊢ ...
12	6	cv	⊢ 𝑛
13	10 12 11	co	⊢ ( 1 ... 𝑛 )
14	1	cv	⊢ 𝑙
15	9	cv	⊢ 𝑎
16	15 14	cfv	⊢ ( 𝑙 ‘ 𝑎 )
17		cmul	⊢ ·
18		ce	⊢ exp
19		ci	⊢ i
20		c2	⊢ 2
21		cpi	⊢ π
22	20 21 17	co	⊢ ( 2 · π )
23	19 22 17	co	⊢ ( i · ( 2 · π ) )
24	8	cv	⊢ 𝑥
25	15 24 17	co	⊢ ( 𝑎 · 𝑥 )
26	23 25 17	co	⊢ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) )
27	26 18	cfv	⊢ ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) )
28	16 27 17	co	⊢ ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) )
29	13 28 9	csu	⊢ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) )
30	8 2 29	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) )
31	1 6 5 7 30	cmpo	⊢ ( 𝑙 ∈ ( ℂ ↑_m ℕ ) , 𝑛 ∈ ℕ₀ ↦ ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) )
32	0 31	wceq	⊢ vts = ( 𝑙 ∈ ( ℂ ↑_m ℕ ) , 𝑛 ∈ ℕ₀ ↦ ( 𝑥 ∈ ℂ ↦ Σ 𝑎 ∈ ( 1 ... 𝑛 ) ( ( 𝑙 ‘ 𝑎 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( 𝑎 · 𝑥 ) ) ) ) ) )

Metamath Proof Explorer