circlevma

Description: The Circle Method, where the Vinogradov sums are weighted using the von Mangoldt function, as it appears as proposition 1.1 of Helfgott p. 5. (Contributed by Thierry Arnoux, 13-Dec-2021)

		Ref	Expression
	Hypothesis	circlevma.n	$⊢ φ \to N \in ℕ_{0}$
	Assertion	circlevma	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) Λ (n (1)) Λ (n (2)) = \int_{(0, 1)} {(Λ vts N) (x)}^{3} e^{i 2 π -N x} d x$

Proof

Step	Hyp	Ref	Expression
1		circlevma.n	$⊢ φ \to N \in ℕ_{0}$
2		3nn	$⊢ 3 \in ℕ$
3	2	a1i	$⊢ φ \to 3 \in ℕ$
4		vmaf	$⊢ Λ : ℕ ⟶ ℝ$
5		ax-resscn	$⊢ ℝ \subseteq ℂ$
6		fss	$⊢ (Λ : ℕ ⟶ ℝ \land ℝ \subseteq ℂ) \to Λ : ℕ ⟶ ℂ$
7	4 5 6	mp2an	$⊢ Λ : ℕ ⟶ ℂ$
8		cnex	$⊢ ℂ \in V$
9		nnex	$⊢ ℕ \in V$
10		elmapg	$⊢ (ℂ \in V \land ℕ \in V) \to (Λ \in (ℂ^{ℕ}) \leftrightarrow Λ : ℕ ⟶ ℂ)$
11	8 9 10	mp2an	$⊢ Λ \in (ℂ^{ℕ}) \leftrightarrow Λ : ℕ ⟶ ℂ$
12	7 11	mpbir	$⊢ Λ \in (ℂ^{ℕ})$
13	12	fconst6	$⊢ ((0 ..^3) \times \{Λ\}) : (0 ..^3) ⟶ ℂ^{ℕ}$
14	13	a1i	$⊢ φ \to ((0 ..^3) \times \{Λ\}) : (0 ..^3) ⟶ ℂ^{ℕ}$
15	1 3 14	circlemeth	$⊢ φ \to \sum_{n \in ℕ repr (3) N} \prod_{a \in (0 ..^3)} ((0 ..^3) \times \{Λ\}) (a) (n (a)) = \int_{(0, 1)} \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) e^{i 2 π -N x} d x$
16		c0ex	$⊢ 0 \in V$
17	16	tpid1	$⊢ 0 \in \{0, 1, 2\}$
18		fzo0to3tp	$⊢ (0 ..^3) = \{0, 1, 2\}$
19	17 18	eleqtrri	$⊢ 0 \in (0 ..^3)$
20		eleq1	$⊢ a = 0 \to (a \in (0 ..^3) \leftrightarrow 0 \in (0 ..^3))$
21	19 20	mpbiri	$⊢ a = 0 \to a \in (0 ..^3)$
22	12	elexi	$⊢ Λ \in V$
23	22	fvconst2	$⊢ a \in (0 ..^3) \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
24	21 23	syl	$⊢ a = 0 \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
25		fveq2	$⊢ a = 0 \to n (a) = n (0)$
26	24 25	fveq12d	$⊢ a = 0 \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (0))$
27		1ex	$⊢ 1 \in V$
28	27	tpid2	$⊢ 1 \in \{0, 1, 2\}$
29	28 18	eleqtrri	$⊢ 1 \in (0 ..^3)$
30		eleq1	$⊢ a = 1 \to (a \in (0 ..^3) \leftrightarrow 1 \in (0 ..^3))$
31	29 30	mpbiri	$⊢ a = 1 \to a \in (0 ..^3)$
32	31 23	syl	$⊢ a = 1 \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
33		fveq2	$⊢ a = 1 \to n (a) = n (1)$
34	32 33	fveq12d	$⊢ a = 1 \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (1))$
35		2ex	$⊢ 2 \in V$
36	35	tpid3	$⊢ 2 \in \{0, 1, 2\}$
37	36 18	eleqtrri	$⊢ 2 \in (0 ..^3)$
38		eleq1	$⊢ a = 2 \to (a \in (0 ..^3) \leftrightarrow 2 \in (0 ..^3))$
39	37 38	mpbiri	$⊢ a = 2 \to a \in (0 ..^3)$
40	39 23	syl	$⊢ a = 2 \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
41		fveq2	$⊢ a = 2 \to n (a) = n (2)$
42	40 41	fveq12d	$⊢ a = 2 \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (2))$
43	23	fveq1d	$⊢ a \in (0 ..^3) \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (a))$
44	43	adantl	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (a))$
45	7	a1i	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to Λ : ℕ ⟶ ℂ$
46		ssidd	$⊢ (φ \land n \in (ℕ repr (3) N)) \to ℕ \subseteq ℕ$
47	1	nn0zd	$⊢ φ \to N \in ℤ$
48	47	adantr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to N \in ℤ$
49	2	nnnn0i	$⊢ 3 \in ℕ_{0}$
50	49	a1i	$⊢ (φ \land n \in (ℕ repr (3) N)) \to 3 \in ℕ_{0}$
51		simpr	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n \in (ℕ repr (3) N)$
52	46 48 50 51	reprf	$⊢ (φ \land n \in (ℕ repr (3) N)) \to n : (0 ..^3) ⟶ ℕ$
53	52	ffvelrnda	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to n (a) \in ℕ$
54	45 53	ffvelrnd	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to Λ (n (a)) \in ℂ$
55	44 54	eqeltrd	$⊢ ((φ \land n \in (ℕ repr (3) N)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) (n (a)) \in ℂ$
56	26 34 42 55	prodfzo03	$⊢ (φ \land n \in (ℕ repr (3) N)) \to \prod_{a \in (0 ..^3)} ((0 ..^3) \times \{Λ\}) (a) (n (a)) = Λ (n (0)) Λ (n (1)) Λ (n (2))$
57	56	sumeq2dv	$⊢ φ \to \sum_{n \in ℕ repr (3) N} \prod_{a \in (0 ..^3)} ((0 ..^3) \times \{Λ\}) (a) (n (a)) = \sum_{n \in ℕ repr (3) N} Λ (n (0)) Λ (n (1)) Λ (n (2))$
58	23	adantl	$⊢ ((φ \land x \in (0, 1)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) = Λ$
59	58	oveq1d	$⊢ ((φ \land x \in (0, 1)) \land a \in (0 ..^3)) \to ((0 ..^3) \times \{Λ\}) (a) vts N = Λ vts N$
60	59	fveq1d	$⊢ ((φ \land x \in (0, 1)) \land a \in (0 ..^3)) \to (((0 ..^3) \times \{Λ\}) (a) vts N) (x) = (Λ vts N) (x)$
61	60	prodeq2dv	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) = \prod_{a \in (0 ..^3)} (Λ vts N) (x)$
62		fzofi	$⊢ (0 ..^3) \in Fin$
63	62	a1i	$⊢ (φ \land x \in (0, 1)) \to (0 ..^3) \in Fin$
64	1	adantr	$⊢ (φ \land x \in (0, 1)) \to N \in ℕ_{0}$
65		ioossre	$⊢ (0, 1) \subseteq ℝ$
66	65 5	sstri	$⊢ (0, 1) \subseteq ℂ$
67	66	a1i	$⊢ φ \to (0, 1) \subseteq ℂ$
68	67	sselda	$⊢ (φ \land x \in (0, 1)) \to x \in ℂ$
69	7	a1i	$⊢ (φ \land x \in (0, 1)) \to Λ : ℕ ⟶ ℂ$
70	64 68 69	vtscl	$⊢ (φ \land x \in (0, 1)) \to (Λ vts N) (x) \in ℂ$
71		fprodconst	$⊢ ((0 ..^3) \in Fin \land (Λ vts N) (x) \in ℂ) \to \prod_{a \in (0 ..^3)} (Λ vts N) (x) = {(Λ vts N) (x)}^{\|(0 ..^3)\|}$
72	63 70 71	syl2anc	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (Λ vts N) (x) = {(Λ vts N) (x)}^{\|(0 ..^3)\|}$
73		hashfzo0	$⊢ 3 \in ℕ_{0} \to \|(0 ..^3)\| = 3$
74	49 73	ax-mp	$⊢ \|(0 ..^3)\| = 3$
75	74	a1i	$⊢ (φ \land x \in (0, 1)) \to \|(0 ..^3)\| = 3$
76	75	oveq2d	$⊢ (φ \land x \in (0, 1)) \to {(Λ vts N) (x)}^{\|(0 ..^3)\|} = {(Λ vts N) (x)}^{3}$
77	61 72 76	3eqtrd	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) = {(Λ vts N) (x)}^{3}$
78	77	oveq1d	$⊢ (φ \land x \in (0, 1)) \to \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) e^{i 2 π -N x} = {(Λ vts N) (x)}^{3} e^{i 2 π -N x}$
79	78	itgeq2dv	$⊢ φ \to \int_{(0, 1)} \prod_{a \in (0 ..^3)} (((0 ..^3) \times \{Λ\}) (a) vts N) (x) e^{i 2 π -N x} d x = \int_{(0, 1)} {(Λ vts N) (x)}^{3} e^{i 2 π -N x} d x$
80	15 57 79	3eqtr3d	$⊢ φ \to \sum_{n \in ℕ repr (3) N} Λ (n (0)) Λ (n (1)) Λ (n (2)) = \int_{(0, 1)} {(Λ vts N) (x)}^{3} e^{i 2 π -N x} d x$

Metamath Proof Explorer

Theorem circlevma

Proof