Metamath Proof Explorer

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 𝑥