vtsprod

Description: Express the Vinogradov trigonometric sums to the power of S (Contributed by Thierry Arnoux, 12-Dec-2021)

	Ref	Expression
Hypotheses	vtsval.n	$⊢ φ \to N \in ℕ_{0}$
	vtsval.x	$⊢ φ \to X \in ℂ$
	vtsprod.s	$⊢ φ \to S \in ℕ_{0}$
	vtsprod.l	$⊢ φ \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
Assertion	vtsprod	$⊢ φ \to \prod_{a \in (0 ..^S)} (L (a) vts N) (X) = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m X}$

Proof

Step	Hyp	Ref	Expression
1		vtsval.n	$⊢ φ \to N \in ℕ_{0}$
2		vtsval.x	$⊢ φ \to X \in ℂ$
3		vtsprod.s	$⊢ φ \to S \in ℕ_{0}$
4		vtsprod.l	$⊢ φ \to L : (0 ..^S) ⟶ ℂ^{ℕ}$
5		ax-icn	$⊢ i \in ℂ$
6	5	a1i	$⊢ φ \to i \in ℂ$
7		2cnd	$⊢ φ \to 2 \in ℂ$
8		picn	$⊢ π \in ℂ$
9	8	a1i	$⊢ φ \to π \in ℂ$
10	7 9	mulcld	$⊢ φ \to 2 π \in ℂ$
11	6 10	mulcld	$⊢ φ \to i 2 π \in ℂ$
12	11 2	mulcld	$⊢ φ \to i 2 π X \in ℂ$
13	12	efcld	$⊢ φ \to e^{i 2 π X} \in ℂ$
14	1 3 13 4	breprexp	$⊢ φ \to \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) {e^{i 2 π X}}^{b} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) {e^{i 2 π X}}^{m}$
15	1	adantr	$⊢ (φ \land a \in (0 ..^S)) \to N \in ℕ_{0}$
16	2	adantr	$⊢ (φ \land a \in (0 ..^S)) \to X \in ℂ$
17	4	ffvelrnda	$⊢ (φ \land a \in (0 ..^S)) \to L (a) \in (ℂ^{ℕ})$
18		elmapi	$⊢ L (a) \in (ℂ^{ℕ}) \to L (a) : ℕ ⟶ ℂ$
19	17 18	syl	$⊢ (φ \land a \in (0 ..^S)) \to L (a) : ℕ ⟶ ℂ$
20	15 16 19	vtsval	$⊢ (φ \land a \in (0 ..^S)) \to (L (a) vts N) (X) = \sum_{b = 1}^{N} L (a) (b) e^{i 2 π b X}$
21		fzssz	$⊢ (1 \dots N) \subseteq ℤ$
22		simpr	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to b \in (1 \dots N)$
23	21 22	sselid	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to b \in ℤ$
24	23	zcnd	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to b \in ℂ$
25	11	ad2antrr	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to i 2 π \in ℂ$
26	16	adantr	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to X \in ℂ$
27	24 25 26	mul12d	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to b i 2 π X = i 2 π b X$
28	27	fveq2d	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to e^{b i 2 π X} = e^{i 2 π b X}$
29	12	ad2antrr	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to i 2 π X \in ℂ$
30		efexp	$⊢ (i 2 π X \in ℂ \land b \in ℤ) \to e^{b i 2 π X} = {e^{i 2 π X}}^{b}$
31	29 23 30	syl2anc	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to e^{b i 2 π X} = {e^{i 2 π X}}^{b}$
32	28 31	eqtr3d	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to e^{i 2 π b X} = {e^{i 2 π X}}^{b}$
33	32	oveq2d	$⊢ ((φ \land a \in (0 ..^S)) \land b \in (1 \dots N)) \to L (a) (b) e^{i 2 π b X} = L (a) (b) {e^{i 2 π X}}^{b}$
34	33	sumeq2dv	$⊢ (φ \land a \in (0 ..^S)) \to \sum_{b = 1}^{N} L (a) (b) e^{i 2 π b X} = \sum_{b = 1}^{N} L (a) (b) {e^{i 2 π X}}^{b}$
35	20 34	eqtrd	$⊢ (φ \land a \in (0 ..^S)) \to (L (a) vts N) (X) = \sum_{b = 1}^{N} L (a) (b) {e^{i 2 π X}}^{b}$
36	35	prodeq2dv	$⊢ φ \to \prod_{a \in (0 ..^S)} (L (a) vts N) (X) = \prod_{a \in (0 ..^S)} \sum_{b = 1}^{N} L (a) (b) {e^{i 2 π X}}^{b}$
37		fzssz	$⊢ (0 \dots S \cdot N) \subseteq ℤ$
38		simpr	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in (0 \dots S \cdot N)$
39	37 38	sselid	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to m \in ℤ$
40	39	adantr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m \in ℤ$
41	40	zcnd	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m \in ℂ$
42	11	ad2antrr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to i 2 π \in ℂ$
43	2	ad2antrr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to X \in ℂ$
44	41 42 43	mul12d	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to m i 2 π X = i 2 π m X$
45	44	fveq2d	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to e^{m i 2 π X} = e^{i 2 π m X}$
46	12	ad2antrr	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to i 2 π X \in ℂ$
47		efexp	$⊢ (i 2 π X \in ℂ \land m \in ℤ) \to e^{m i 2 π X} = {e^{i 2 π X}}^{m}$
48	46 40 47	syl2anc	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to e^{m i 2 π X} = {e^{i 2 π X}}^{m}$
49	45 48	eqtr3d	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to e^{i 2 π m X} = {e^{i 2 π X}}^{m}$
50	49	oveq2d	$⊢ ((φ \land m \in (0 \dots S \cdot N)) \land c \in ((1 \dots N) repr (S) m)) \to \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m X} = \prod_{a \in (0 ..^S)} L (a) (c (a)) {e^{i 2 π X}}^{m}$
51	50	sumeq2dv	$⊢ (φ \land m \in (0 \dots S \cdot N)) \to \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m X} = \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) {e^{i 2 π X}}^{m}$
52	51	sumeq2dv	$⊢ φ \to \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m X} = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) {e^{i 2 π X}}^{m}$
53	14 36 52	3eqtr4d	$⊢ φ \to \prod_{a \in (0 ..^S)} (L (a) vts N) (X) = \sum_{m = 0}^{S \cdot N} \sum_{c \in (1 \dots N) repr (S) m} \prod_{a \in (0 ..^S)} L (a) (c (a)) e^{i 2 π m X}$

Metamath Proof Explorer

Theorem vtsprod

Proof