Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-vts Structured version   Visualization version   GIF version

Definition df-vts 32021
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
StepHypRef Expression
1 cvts 32020 . 2 class vts
2 vl . . 3 setvar 𝑙
3 vn . . 3 setvar 𝑛
4 cc 10528 . . . 4 class
5 cn 11629 . . . 4 class
6 cmap 8393 . . . 4 class m
74, 5, 6co 7139 . . 3 class (ℂ ↑m ℕ)
8 cn0 11889 . . 3 class 0
9 vx . . . 4 setvar 𝑥
10 c1 10531 . . . . . 6 class 1
113cv 1537 . . . . . 6 class 𝑛
12 cfz 12889 . . . . . 6 class ...
1310, 11, 12co 7139 . . . . 5 class (1...𝑛)
14 va . . . . . . . 8 setvar 𝑎
1514cv 1537 . . . . . . 7 class 𝑎
162cv 1537 . . . . . . 7 class 𝑙
1715, 16cfv 6328 . . . . . 6 class (𝑙𝑎)
18 ci 10532 . . . . . . . . 9 class i
19 c2 11684 . . . . . . . . . 10 class 2
20 cpi 15416 . . . . . . . . . 10 class π
21 cmul 10535 . . . . . . . . . 10 class ·
2219, 20, 21co 7139 . . . . . . . . 9 class (2 · π)
2318, 22, 21co 7139 . . . . . . . 8 class (i · (2 · π))
249cv 1537 . . . . . . . . 9 class 𝑥
2515, 24, 21co 7139 . . . . . . . 8 class (𝑎 · 𝑥)
2623, 25, 21co 7139 . . . . . . 7 class ((i · (2 · π)) · (𝑎 · 𝑥))
27 ce 15411 . . . . . . 7 class exp
2826, 27cfv 6328 . . . . . 6 class (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))
2917, 28, 21co 7139 . . . . 5 class ((𝑙𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))
3013, 29, 14csu 15038 . . . 4 class Σ𝑎 ∈ (1...𝑛)((𝑙𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))
319, 4, 30cmpt 5113 . . 3 class (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥)))))
322, 3, 7, 8, 31cmpo 7141 . 2 class (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
331, 32wceq 1538 1 wff vts = (𝑙 ∈ (ℂ ↑m ℕ), 𝑛 ∈ ℕ0 ↦ (𝑥 ∈ ℂ ↦ Σ𝑎 ∈ (1...𝑛)((𝑙𝑎) · (exp‘((i · (2 · π)) · (𝑎 · 𝑥))))))
Colors of variables: wff setvar class
This definition is referenced by:  vtsval  32022
  Copyright terms: Public domain W3C validator