Theorem vtsval

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

	Ref	Expression
Hypotheses	vtsval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	vtsval.x	$$⊢\phi \to X\in ℂ$$
	vtsval.l	$$⊢\phi \to L:\mathbb{N}⟶ℂ$$
Assertion	vtsval	$$⊢\phi \to \left(L\mathrm{vts}N\right)\left(X\right)=\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}$$

Proof

Step	Hyp	Ref	Expression
1		vtsval.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		vtsval.x	$$⊢\phi \to X\in ℂ$$
3		vtsval.l	$$⊢\phi \to L:\mathbb{N}⟶ℂ$$
4		cnex	$$⊢ℂ\in \mathrm{V}$$
5		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
6	4 5	elmap	$$⊢L\in \left({ℂ}^{\mathbb{N}}\right)\leftrightarrow L:\mathbb{N}⟶ℂ$$
7	3 6	sylibr	$$⊢\phi \to L\in \left({ℂ}^{\mathbb{N}}\right)$$
8		fveq1	$$⊢l=L\to l\left(a\right)=L\left(a\right)$$
9	8	oveq1d	$$⊢l=L\to l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}=L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}$$
10	9	sumeq2sdv	$$⊢l=L\to \sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}=\sum _{a=1}^{n}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}$$
11	10	mpteq2dv	$$⊢l=L\to \left(x\in ℂ⟼\sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)=\left(x\in ℂ⟼\sum _{a=1}^{n}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)$$
12		oveq2	$$⊢n=N\to \left(1\dots n\right)=\left(1\dots N\right)$$
13	12	sumeq1d	$$⊢n=N\to \sum _{a=1}^{n}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}=\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}$$
14	13	mpteq2dv	$$⊢n=N\to \left(x\in ℂ⟼\sum _{a=1}^{n}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)=\left(x\in ℂ⟼\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)$$
15		df-vts	$$⊢\mathrm{vts}=\left(l\in \left({ℂ}^{\mathbb{N}}\right),n\in {\mathbb{N}}_0⟼\left(x\in ℂ⟼\sum _{a=1}^{n}l\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)\right)$$
16	4	mptex	$$⊢\left(x\in ℂ⟼\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)\in \mathrm{V}$$
17	11 14 15 16	ovmpo	$$⊢\left(L\in \left({ℂ}^{\mathbb{N}}\right)\wedge N\in {\mathbb{N}}_0\right)\to L\mathrm{vts}N=\left(x\in ℂ⟼\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)$$
18	7 1 17	syl2anc	$$⊢\phi \to L\mathrm{vts}N=\left(x\in ℂ⟼\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}\right)$$
19		oveq2	$$⊢x=X\to ax=aX$$
20	19	oveq2d	$$⊢x=X\to \mathrm{i}2\mathrm{\pi }ax=\mathrm{i}2\mathrm{\pi }aX$$
21	20	fveq2d	$$⊢x=X\to {\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}={\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}$$
22	21	oveq2d	$$⊢x=X\to L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}=L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}$$
23	22	sumeq2sdv	$$⊢x=X\to \sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}=\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}$$
24	23	adantl	$$⊢\left(\phi \wedge x=X\right)\to \sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }ax}=\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}$$
25		sumex	$$⊢\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}\in \mathrm{V}$$
26	25	a1i	$$⊢\phi \to \sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}\in \mathrm{V}$$
27	18 24 2 26	fvmptd	$$⊢\phi \to \left(L\mathrm{vts}N\right)\left(X\right)=\sum _{a=1}^{N}L\left(a\right){\mathrm{e}}^{\mathrm{i}2\mathrm{\pi }aX}$$