Theorem 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	⊢ 𝑅 = ( ♯ ‘ ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) )
	circlemethnat.f	⊢ 𝐹 = ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) vts 𝑁 ) ‘ 𝑥 )
	circlemethnat.n	⊢ 𝑁 ∈ ℕ0
	circlemethnat.a	⊢ 𝐴 ⊆ ℕ
	circlemethnat.s	⊢ 𝑆 ∈ ℕ
Assertion	circlemethnat	⊢ 𝑅 = ∫ ( 0 (,) 1 ) ( ( 𝐹 ↑ 𝑆 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥

Proof

Step	Hyp	Ref	Expression
1		circlemethnat.r	⊢ 𝑅 = ( ♯ ‘ ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) )
2		circlemethnat.f	⊢ 𝐹 = ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) vts 𝑁 ) ‘ 𝑥 )
3		circlemethnat.n	⊢ 𝑁 ∈ ℕ0
4		circlemethnat.a	⊢ 𝐴 ⊆ ℕ
5		circlemethnat.s	⊢ 𝑆 ∈ ℕ
6		nnex	⊢ ℕ ∈ V
7		indf	⊢ ( ( ℕ ∈ V ∧ 𝐴 ⊆ ℕ ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } )
8	6 4 7	mp2an	⊢ ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 }
9		pr01ssre	⊢ { 0 , 1 } ⊆ ℝ
10		ax-resscn	⊢ ℝ ⊆ ℂ
11	9 10	sstri	⊢ { 0 , 1 } ⊆ ℂ
12		fss	⊢ ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℂ ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ ℂ )
13	8 11 12	mp2an	⊢ ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ ℂ
14		cnex	⊢ ℂ ∈ V
15	14 6	elmap	⊢ ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ∈ ( ℂ ↑m ℕ ) ↔ ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ ℂ )
16	13 15	mpbir	⊢ ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ∈ ( ℂ ↑m ℕ )
17	16	elexi	⊢ ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ∈ V
18	17	fvconst2	⊢ ( 𝑎 ∈ ( 0 ..^ 𝑆 ) → ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) = ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) )
19	18	adantl	⊢ ( ( ( ⊤ ∧ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) = ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) )
20	19	fveq1d	⊢ ( ( ( ⊤ ∧ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
21	20	prodeq2dv	⊢ ( ( ⊤ ∧ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
22	21	sumeq2dv	⊢ ( ⊤ → Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
23	4	a1i	⊢ ( ⊤ → 𝐴 ⊆ ℕ )
24	3	a1i	⊢ ( ⊤ → 𝑁 ∈ ℕ0 )
25	5	a1i	⊢ ( ⊤ → 𝑆 ∈ ℕ )
26	25	nnnn0d	⊢ ( ⊤ → 𝑆 ∈ ℕ0 )
27	23 24 26	hashrepr	⊢ ( ⊤ → ( ♯ ‘ ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) ) = Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
28	22 27	eqtr4d	⊢ ( ⊤ → Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = ( ♯ ‘ ( 𝐴 ( repr ‘ 𝑆 ) 𝑁 ) ) )
29	1 28	eqtr4id	⊢ ( ⊤ → 𝑅 = Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) )
30	16	fconst6	⊢ ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ )
31	30	a1i	⊢ ( ⊤ → ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
32	24 25 31	circlemeth	⊢ ( ⊤ → Σ 𝑐 ∈ ( ℕ ( repr ‘ 𝑆 ) 𝑁 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) = ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
33		fzofi	⊢ ( 0 ..^ 𝑆 ) ∈ Fin
34	33	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
35	3	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑁 ∈ ℕ0 )
36		ioossre	⊢ ( 0 (,) 1 ) ⊆ ℝ
37	36 10	sstri	⊢ ( 0 (,) 1 ) ⊆ ℂ
38	37	a1i	⊢ ( ⊤ → ( 0 (,) 1 ) ⊆ ℂ )
39	38	sselda	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑥 ∈ ℂ )
40	13	a1i	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ ℂ )
41	35 39 40	vtscl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) vts 𝑁 ) ‘ 𝑥 ) ∈ ℂ )
42	2 41	eqeltrid	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝐹 ∈ ℂ )
43		fprodconst	⊢ ( ( ( 0 ..^ 𝑆 ) ∈ Fin ∧ 𝐹 ∈ ℂ ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝐹 = ( 𝐹 ↑ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ) )
44	34 42 43	syl2anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝐹 = ( 𝐹 ↑ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ) )
45	18	adantl	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) = ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) )
46	45	oveq1d	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) = ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) vts 𝑁 ) )
47	46	fveq1d	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) vts 𝑁 ) ‘ 𝑥 ) )
48	2 47	eqtr4id	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐹 = ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) )
49	48	prodeq2dv	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) 𝐹 = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) )
50	26	adantr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → 𝑆 ∈ ℕ0 )
51		hashfzo0	⊢ ( 𝑆 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
52	50 51	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
53	52	oveq2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( 𝐹 ↑ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ) = ( 𝐹 ↑ 𝑆 ) )
54	44 49 53	3eqtr3d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) = ( 𝐹 ↑ 𝑆 ) )
55	54	oveq1d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 0 (,) 1 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) = ( ( 𝐹 ↑ 𝑆 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) )
56	55	itgeq2dv	⊢ ( ⊤ → ∫ ( 0 (,) 1 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) vts 𝑁 ) ‘ 𝑥 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 = ∫ ( 0 (,) 1 ) ( ( 𝐹 ↑ 𝑆 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
57	29 32 56	3eqtrd	⊢ ( ⊤ → 𝑅 = ∫ ( 0 (,) 1 ) ( ( 𝐹 ↑ 𝑆 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥 )
58	57	mptru	⊢ 𝑅 = ∫ ( 0 (,) 1 ) ( ( 𝐹 ↑ 𝑆 ) · ( exp ‘ ( ( i · ( 2 · π ) ) · ( - 𝑁 · 𝑥 ) ) ) ) d 𝑥