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 
|- R = ( # ` ( A ( repr ` S ) N ) )
circlemethnat.f 
|- F = ( ( ( ( _Ind ` NN ) ` A ) vts N ) ` x )
circlemethnat.n 
|- N e. NN0
circlemethnat.a 
|- A C_ NN
circlemethnat.s 
|- S e. NN
Assertion circlemethnat 
|- R = S. ( 0 (,) 1 ) ( ( F ^ S ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x

Proof

Step Hyp Ref Expression
1 circlemethnat.r 
 |-  R = ( # ` ( A ( repr ` S ) N ) )
2 circlemethnat.f 
 |-  F = ( ( ( ( _Ind ` NN ) ` A ) vts N ) ` x )
3 circlemethnat.n 
 |-  N e. NN0
4 circlemethnat.a 
 |-  A C_ NN
5 circlemethnat.s 
 |-  S e. NN
6 nnex 
 |-  NN e. _V
7 indf 
 |-  ( ( NN e. _V /\ A C_ NN ) -> ( ( _Ind ` NN ) ` A ) : NN --> { 0 , 1 } )
8 6 4 7 mp2an 
 |-  ( ( _Ind ` NN ) ` A ) : NN --> { 0 , 1 }
9 pr01ssre 
 |-  { 0 , 1 } C_ RR
10 ax-resscn 
 |-  RR C_ CC
11 9 10 sstri 
 |-  { 0 , 1 } C_ CC
12 fss 
 |-  ( ( ( ( _Ind ` NN ) ` A ) : NN --> { 0 , 1 } /\ { 0 , 1 } C_ CC ) -> ( ( _Ind ` NN ) ` A ) : NN --> CC )
13 8 11 12 mp2an 
 |-  ( ( _Ind ` NN ) ` A ) : NN --> CC
14 cnex 
 |-  CC e. _V
15 14 6 elmap 
 |-  ( ( ( _Ind ` NN ) ` A ) e. ( CC ^m NN ) <-> ( ( _Ind ` NN ) ` A ) : NN --> CC )
16 13 15 mpbir 
 |-  ( ( _Ind ` NN ) ` A ) e. ( CC ^m NN )
17 16 elexi 
 |-  ( ( _Ind ` NN ) ` A ) e. _V
18 17 fvconst2 
 |-  ( a e. ( 0 ..^ S ) -> ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) = ( ( _Ind ` NN ) ` A ) )
19 18 adantl 
 |-  ( ( ( T. /\ c e. ( NN ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) = ( ( _Ind ` NN ) ` A ) )
20 19 fveq1d 
 |-  ( ( ( T. /\ c e. ( NN ( repr ` S ) N ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
21 20 prodeq2dv 
 |-  ( ( T. /\ c e. ( NN ( repr ` S ) N ) ) -> prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
22 21 sumeq2dv 
 |-  ( T. -> sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
23 4 a1i 
 |-  ( T. -> A C_ NN )
24 3 a1i 
 |-  ( T. -> N e. NN0 )
25 5 a1i 
 |-  ( T. -> S e. NN )
26 25 nnnn0d 
 |-  ( T. -> S e. NN0 )
27 23 24 26 hashrepr 
 |-  ( T. -> ( # ` ( A ( repr ` S ) N ) ) = sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( ( _Ind ` NN ) ` A ) ` ( c ` a ) ) )
28 22 27 eqtr4d 
 |-  ( T. -> sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = ( # ` ( A ( repr ` S ) N ) ) )
29 1 28 eqtr4id 
 |-  ( T. -> R = sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) )
30 16 fconst6 
 |-  ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) : ( 0 ..^ S ) --> ( CC ^m NN )
31 30 a1i 
 |-  ( T. -> ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) : ( 0 ..^ S ) --> ( CC ^m NN ) )
32 24 25 31 circlemeth 
 |-  ( T. -> sum_ c e. ( NN ( repr ` S ) N ) prod_ a e. ( 0 ..^ S ) ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) ` ( c ` a ) ) = S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
33 fzofi 
 |-  ( 0 ..^ S ) e. Fin
34 33 a1i 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> ( 0 ..^ S ) e. Fin )
35 3 a1i 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> N e. NN0 )
36 ioossre 
 |-  ( 0 (,) 1 ) C_ RR
37 36 10 sstri 
 |-  ( 0 (,) 1 ) C_ CC
38 37 a1i 
 |-  ( T. -> ( 0 (,) 1 ) C_ CC )
39 38 sselda 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> x e. CC )
40 13 a1i 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> ( ( _Ind ` NN ) ` A ) : NN --> CC )
41 35 39 40 vtscl 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> ( ( ( ( _Ind ` NN ) ` A ) vts N ) ` x ) e. CC )
42 2 41 eqeltrid 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> F e. CC )
43 fprodconst 
 |-  ( ( ( 0 ..^ S ) e. Fin /\ F e. CC ) -> prod_ a e. ( 0 ..^ S ) F = ( F ^ ( # ` ( 0 ..^ S ) ) ) )
44 34 42 43 syl2anc 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ S ) F = ( F ^ ( # ` ( 0 ..^ S ) ) ) )
45 18 adantl 
 |-  ( ( ( T. /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) = ( ( _Ind ` NN ) ` A ) )
46 45 oveq1d 
 |-  ( ( ( T. /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) = ( ( ( _Ind ` NN ) ` A ) vts N ) )
47 46 fveq1d 
 |-  ( ( ( T. /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ S ) ) -> ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) ` x ) = ( ( ( ( _Ind ` NN ) ` A ) vts N ) ` x ) )
48 2 47 eqtr4id 
 |-  ( ( ( T. /\ x e. ( 0 (,) 1 ) ) /\ a e. ( 0 ..^ S ) ) -> F = ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) ` x ) )
49 48 prodeq2dv 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ S ) F = prod_ a e. ( 0 ..^ S ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) ` x ) )
50 26 adantr 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> S e. NN0 )
51 hashfzo0 
 |-  ( S e. NN0 -> ( # ` ( 0 ..^ S ) ) = S )
52 50 51 syl 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> ( # ` ( 0 ..^ S ) ) = S )
53 52 oveq2d 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> ( F ^ ( # ` ( 0 ..^ S ) ) ) = ( F ^ S ) )
54 44 49 53 3eqtr3d 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> prod_ a e. ( 0 ..^ S ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) ` x ) = ( F ^ S ) )
55 54 oveq1d 
 |-  ( ( T. /\ x e. ( 0 (,) 1 ) ) -> ( prod_ a e. ( 0 ..^ S ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) = ( ( F ^ S ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
56 55 itgeq2dv 
 |-  ( T. -> S. ( 0 (,) 1 ) ( prod_ a e. ( 0 ..^ S ) ( ( ( ( ( 0 ..^ S ) X. { ( ( _Ind ` NN ) ` A ) } ) ` a ) vts N ) ` x ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x = S. ( 0 (,) 1 ) ( ( F ^ S ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
57 29 32 56 3eqtrd 
 |-  ( T. -> R = S. ( 0 (,) 1 ) ( ( F ^ S ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
58 57 mptru 
 |-  R = S. ( 0 (,) 1 ) ( ( F ^ S ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x