circlemethnat

Description: The Hardy, Littlewood and Ramanujan Circle Method, Chapter 5.1 of Nathanson p. 123. This expresses R , the number of different ways a nonnegative integer N can be represented as the sum of at most S integers in the set A as an integral of Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 13-Dec-2021)

	Ref	Expression
Hypotheses	circlemethnat.r	$⊢ R = \|A repr (S) N\|$
	circlemethnat.f	$⊢ F = (𝟙_{ℕ} (A) vts N) (x)$
	circlemethnat.n	$⊢ N \in ℕ_{0}$
	circlemethnat.a	$⊢ A \subseteq ℕ$
	circlemethnat.s	$⊢ S \in ℕ$
Assertion	circlemethnat	$⊢ R = \int_{(0, 1)} F^{S} e^{i 2 π -N x} d x$

Proof

Step	Hyp	Ref	Expression
1		circlemethnat.r	$⊢ R = \|A repr (S) N\|$
2		circlemethnat.f	$⊢ F = (𝟙_{ℕ} (A) vts N) (x)$
3		circlemethnat.n	$⊢ N \in ℕ_{0}$
4		circlemethnat.a	$⊢ A \subseteq ℕ$
5		circlemethnat.s	$⊢ S \in ℕ$
6		nnex	$⊢ ℕ \in V$
7		indf	$⊢ (ℕ \in V \land A \subseteq ℕ) \to 𝟙_{ℕ} (A) : ℕ ⟶ \{0, 1\}$
8	6 4 7	mp2an	$⊢ 𝟙_{ℕ} (A) : ℕ ⟶ \{0, 1\}$
9		pr01ssre	$⊢ \{0, 1\} \subseteq ℝ$
10		ax-resscn	$⊢ ℝ \subseteq ℂ$
11	9 10	sstri	$⊢ \{0, 1\} \subseteq ℂ$
12		fss	$⊢ (𝟙_{ℕ} (A) : ℕ ⟶ \{0, 1\} \land \{0, 1\} \subseteq ℂ) \to 𝟙_{ℕ} (A) : ℕ ⟶ ℂ$
13	8 11 12	mp2an	$⊢ 𝟙_{ℕ} (A) : ℕ ⟶ ℂ$
14		cnex	$⊢ ℂ \in V$
15	14 6	elmap	$⊢ 𝟙_{ℕ} (A) \in (ℂ^{ℕ}) \leftrightarrow 𝟙_{ℕ} (A) : ℕ ⟶ ℂ$
16	13 15	mpbir	$⊢ 𝟙_{ℕ} (A) \in (ℂ^{ℕ})$
17	16	elexi	$⊢ 𝟙_{ℕ} (A) \in V$
18	17	fvconst2	$⊢ a \in (0 ..^S) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) = 𝟙_{ℕ} (A)$
19	18	adantl	$⊢ ((⊤ \land c \in (ℕ repr (S) N)) \land a \in (0 ..^S)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) = 𝟙_{ℕ} (A)$
20	19	fveq1d	$⊢ ((⊤ \land c \in (ℕ repr (S) N)) \land a \in (0 ..^S)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = 𝟙_{ℕ} (A) (c (a))$
21	20	prodeq2dv	$⊢ (⊤ \land c \in (ℕ repr (S) N)) \to \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
22	21	sumeq2dv	$⊢ ⊤ \to \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
23	4	a1i	$⊢ ⊤ \to A \subseteq ℕ$
24	3	a1i	$⊢ ⊤ \to N \in ℕ_{0}$
25	5	a1i	$⊢ ⊤ \to S \in ℕ$
26	25	nnnn0d	$⊢ ⊤ \to S \in ℕ_{0}$
27	23 24 26	hashrepr	$⊢ ⊤ \to \|A repr (S) N\| = \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} 𝟙_{ℕ} (A) (c (a))$
28	22 27	eqtr4d	$⊢ ⊤ \to \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = \|A repr (S) N\|$
29	1 28	eqtr4id	$⊢ ⊤ \to R = \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a))$
30	16	fconst6	$⊢ ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) : (0 ..^S) ⟶ ℂ^{ℕ}$
31	30	a1i	$⊢ ⊤ \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) : (0 ..^S) ⟶ ℂ^{ℕ}$
32	24 25 31	circlemeth	$⊢ ⊤ \to \sum_{c \in ℕ repr (S) N} \prod_{a \in (0 ..^S)} ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) (c (a)) = \int_{(0, 1)} \prod_{a \in (0 ..^S)} (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N) (x) e^{i 2 π -N x} d x$
33		fzofi	$⊢ (0 ..^S) \in Fin$
34	33	a1i	$⊢ (⊤ \land x \in (0, 1)) \to (0 ..^S) \in Fin$
35	3	a1i	$⊢ (⊤ \land x \in (0, 1)) \to N \in ℕ_{0}$
36		ioossre	$⊢ (0, 1) \subseteq ℝ$
37	36 10	sstri	$⊢ (0, 1) \subseteq ℂ$
38	37	a1i	$⊢ ⊤ \to (0, 1) \subseteq ℂ$
39	38	sselda	$⊢ (⊤ \land x \in (0, 1)) \to x \in ℂ$
40	13	a1i	$⊢ (⊤ \land x \in (0, 1)) \to 𝟙_{ℕ} (A) : ℕ ⟶ ℂ$
41	35 39 40	vtscl	$⊢ (⊤ \land x \in (0, 1)) \to (𝟙_{ℕ} (A) vts N) (x) \in ℂ$
42	2 41	eqeltrid	$⊢ (⊤ \land x \in (0, 1)) \to F \in ℂ$
43		fprodconst	$⊢ ((0 ..^S) \in Fin \land F \in ℂ) \to \prod_{a \in (0 ..^S)} F = F^{\|(0 ..^S)\|}$
44	34 42 43	syl2anc	$⊢ (⊤ \land x \in (0, 1)) \to \prod_{a \in (0 ..^S)} F = F^{\|(0 ..^S)\|}$
45	18	adantl	$⊢ ((⊤ \land x \in (0, 1)) \land a \in (0 ..^S)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) = 𝟙_{ℕ} (A)$
46	45	oveq1d	$⊢ ((⊤ \land x \in (0, 1)) \land a \in (0 ..^S)) \to ((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N = 𝟙_{ℕ} (A) vts N$
47	46	fveq1d	$⊢ ((⊤ \land x \in (0, 1)) \land a \in (0 ..^S)) \to (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N) (x) = (𝟙_{ℕ} (A) vts N) (x)$
48	2 47	eqtr4id	$⊢ ((⊤ \land x \in (0, 1)) \land a \in (0 ..^S)) \to F = (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N) (x)$
49	48	prodeq2dv	$⊢ (⊤ \land x \in (0, 1)) \to \prod_{a \in (0 ..^S)} F = \prod_{a \in (0 ..^S)} (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N) (x)$
50	26	adantr	$⊢ (⊤ \land x \in (0, 1)) \to S \in ℕ_{0}$
51		hashfzo0	$⊢ S \in ℕ_{0} \to \|(0 ..^S)\| = S$
52	50 51	syl	$⊢ (⊤ \land x \in (0, 1)) \to \|(0 ..^S)\| = S$
53	52	oveq2d	$⊢ (⊤ \land x \in (0, 1)) \to F^{\|(0 ..^S)\|} = F^{S}$
54	44 49 53	3eqtr3d	$⊢ (⊤ \land x \in (0, 1)) \to \prod_{a \in (0 ..^S)} (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N) (x) = F^{S}$
55	54	oveq1d	$⊢ (⊤ \land x \in (0, 1)) \to \prod_{a \in (0 ..^S)} (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N) (x) e^{i 2 π -N x} = F^{S} e^{i 2 π -N x}$
56	55	itgeq2dv	$⊢ ⊤ \to \int_{(0, 1)} \prod_{a \in (0 ..^S)} (((0 ..^S) \times \{𝟙_{ℕ} (A)\}) (a) vts N) (x) e^{i 2 π -N x} d x = \int_{(0, 1)} F^{S} e^{i 2 π -N x} d x$
57	29 32 56	3eqtrd	$⊢ ⊤ \to R = \int_{(0, 1)} F^{S} e^{i 2 π -N x} d x$
58	57	mptru	$⊢ R = \int_{(0, 1)} F^{S} e^{i 2 π -N x} d x$

Metamath Proof Explorer

Theorem circlemethnat

Proof