Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > circlemethnat | Structured version Visualization version GIF version |
Description: The Hardy, Littlewood and Ramanujan Circle Method, Chapter 5.1 of [Nathanson] p. 123. This expresses 𝑅, the number of different ways a nonnegative integer 𝑁 can be represented as the sum of at most 𝑆 integers in the set 𝐴 as an integral of Vinogradov trigonometric sums. (Contributed by Thierry Arnoux, 13-Dec-2021.) |
Ref | Expression |
---|---|
circlemethnat.r | ⊢ 𝑅 = (♯‘(𝐴(repr‘𝑆)𝑁)) |
circlemethnat.f | ⊢ 𝐹 = ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥) |
circlemethnat.n | ⊢ 𝑁 ∈ ℕ0 |
circlemethnat.a | ⊢ 𝐴 ⊆ ℕ |
circlemethnat.s | ⊢ 𝑆 ∈ ℕ |
Ref | Expression |
---|---|
circlemethnat | ⊢ 𝑅 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | circlemethnat.r | . . . 4 ⊢ 𝑅 = (♯‘(𝐴(repr‘𝑆)𝑁)) | |
2 | nnex 12049 | . . . . . . . . . . . . . 14 ⊢ ℕ ∈ V | |
3 | circlemethnat.a | . . . . . . . . . . . . . 14 ⊢ 𝐴 ⊆ ℕ | |
4 | indf 32089 | . . . . . . . . . . . . . 14 ⊢ ((ℕ ∈ V ∧ 𝐴 ⊆ ℕ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}) | |
5 | 2, 3, 4 | mp2an 689 | . . . . . . . . . . . . 13 ⊢ ((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1} |
6 | pr01ssre 31246 | . . . . . . . . . . . . . 14 ⊢ {0, 1} ⊆ ℝ | |
7 | ax-resscn 10998 | . . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ | |
8 | 6, 7 | sstri 3939 | . . . . . . . . . . . . 13 ⊢ {0, 1} ⊆ ℂ |
9 | fss 6652 | . . . . . . . . . . . . 13 ⊢ ((((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆ ℂ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) | |
10 | 5, 8, 9 | mp2an 689 | . . . . . . . . . . . 12 ⊢ ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ |
11 | cnex 11022 | . . . . . . . . . . . . 13 ⊢ ℂ ∈ V | |
12 | 11, 2 | elmap 8705 | . . . . . . . . . . . 12 ⊢ (((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m ℕ) ↔ ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
13 | 10, 12 | mpbir 230 | . . . . . . . . . . 11 ⊢ ((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m ℕ) |
14 | 13 | elexi 3460 | . . . . . . . . . 10 ⊢ ((𝟭‘ℕ)‘𝐴) ∈ V |
15 | 14 | fvconst2 7116 | . . . . . . . . 9 ⊢ (𝑎 ∈ (0..^𝑆) → (((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴)) |
16 | 15 | adantl 482 | . . . . . . . 8 ⊢ (((⊤ ∧ 𝑐 ∈ (ℕ(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴)) |
17 | 16 | fveq1d 6811 | . . . . . . 7 ⊢ (((⊤ ∧ 𝑐 ∈ (ℕ(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → ((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
18 | 17 | prodeq2dv 15702 | . . . . . 6 ⊢ ((⊤ ∧ 𝑐 ∈ (ℕ(repr‘𝑆)𝑁)) → ∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
19 | 18 | sumeq2dv 15484 | . . . . 5 ⊢ (⊤ → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
20 | 3 | a1i 11 | . . . . . 6 ⊢ (⊤ → 𝐴 ⊆ ℕ) |
21 | circlemethnat.n | . . . . . . 7 ⊢ 𝑁 ∈ ℕ0 | |
22 | 21 | a1i 11 | . . . . . 6 ⊢ (⊤ → 𝑁 ∈ ℕ0) |
23 | circlemethnat.s | . . . . . . . 8 ⊢ 𝑆 ∈ ℕ | |
24 | 23 | a1i 11 | . . . . . . 7 ⊢ (⊤ → 𝑆 ∈ ℕ) |
25 | 24 | nnnn0d 12363 | . . . . . 6 ⊢ (⊤ → 𝑆 ∈ ℕ0) |
26 | 20, 22, 25 | hashrepr 32711 | . . . . 5 ⊢ (⊤ → (♯‘(𝐴(repr‘𝑆)𝑁)) = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
27 | 19, 26 | eqtr4d 2780 | . . . 4 ⊢ (⊤ → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (♯‘(𝐴(repr‘𝑆)𝑁))) |
28 | 1, 27 | eqtr4id 2796 | . . 3 ⊢ (⊤ → 𝑅 = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎))) |
29 | 13 | fconst6 6699 | . . . . 5 ⊢ ((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑m ℕ) |
30 | 29 | a1i 11 | . . . 4 ⊢ (⊤ → ((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑m ℕ)) |
31 | 22, 24, 30 | circlemeth 32726 | . . 3 ⊢ (⊤ → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥) |
32 | fzofi 13764 | . . . . . . . 8 ⊢ (0..^𝑆) ∈ Fin | |
33 | 32 | a1i 11 | . . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (0..^𝑆) ∈ Fin) |
34 | circlemethnat.f | . . . . . . . 8 ⊢ 𝐹 = ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥) | |
35 | 21 | a1i 11 | . . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝑁 ∈ ℕ0) |
36 | ioossre 13210 | . . . . . . . . . . . 12 ⊢ (0(,)1) ⊆ ℝ | |
37 | 36, 7 | sstri 3939 | . . . . . . . . . . 11 ⊢ (0(,)1) ⊆ ℂ |
38 | 37 | a1i 11 | . . . . . . . . . 10 ⊢ (⊤ → (0(,)1) ⊆ ℂ) |
39 | 38 | sselda 3930 | . . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ) |
40 | 10 | a1i 11 | . . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
41 | 35, 39, 40 | vtscl 32724 | . . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥) ∈ ℂ) |
42 | 34, 41 | eqeltrid 2842 | . . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝐹 ∈ ℂ) |
43 | fprodconst 15757 | . . . . . . 7 ⊢ (((0..^𝑆) ∈ Fin ∧ 𝐹 ∈ ℂ) → ∏𝑎 ∈ (0..^𝑆)𝐹 = (𝐹↑(♯‘(0..^𝑆)))) | |
44 | 33, 42, 43 | syl2anc 584 | . . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)𝐹 = (𝐹↑(♯‘(0..^𝑆)))) |
45 | 15 | adantl 482 | . . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → (((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴)) |
46 | 45 | oveq1d 7328 | . . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → ((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁) = (((𝟭‘ℕ)‘𝐴)vts𝑁)) |
47 | 46 | fveq1d 6811 | . . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → (((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) = ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥)) |
48 | 34, 47 | eqtr4id 2796 | . . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐹 = (((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥)) |
49 | 48 | prodeq2dv 15702 | . . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)𝐹 = ∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥)) |
50 | 25 | adantr 481 | . . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝑆 ∈ ℕ0) |
51 | hashfzo0 14214 | . . . . . . . 8 ⊢ (𝑆 ∈ ℕ0 → (♯‘(0..^𝑆)) = 𝑆) | |
52 | 50, 51 | syl 17 | . . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (♯‘(0..^𝑆)) = 𝑆) |
53 | 52 | oveq2d 7329 | . . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (𝐹↑(♯‘(0..^𝑆))) = (𝐹↑𝑆)) |
54 | 44, 49, 53 | 3eqtr3d 2785 | . . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) = (𝐹↑𝑆)) |
55 | 54 | oveq1d 7328 | . . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = ((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥))))) |
56 | 55 | itgeq2dv 25017 | . . 3 ⊢ (⊤ → ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥) |
57 | 28, 31, 56 | 3eqtrd 2781 | . 2 ⊢ (⊤ → 𝑅 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥) |
58 | 57 | mptru 1547 | 1 ⊢ 𝑅 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥 |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1540 ⊤wtru 1541 ∈ wcel 2105 Vcvv 3441 ⊆ wss 3896 {csn 4569 {cpr 4571 × cxp 5603 ⟶wf 6459 ‘cfv 6463 (class class class)co 7313 ↑m cmap 8661 Fincfn 8779 ℂcc 10939 ℝcr 10940 0cc0 10941 1c1 10942 ici 10943 · cmul 10946 -cneg 11276 ℕcn 12043 2c2 12098 ℕ0cn0 12303 (,)cioo 13149 ..^cfzo 13452 ↑cexp 13852 ♯chash 14114 Σcsu 15466 ∏cprod 15684 expce 15840 πcpi 15845 ∫citg 24853 𝟭cind 32084 reprcrepr 32694 vtscvts 32721 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-rep 5222 ax-sep 5236 ax-nul 5243 ax-pow 5301 ax-pr 5365 ax-un 7626 ax-inf2 9467 ax-cc 10261 ax-cnex 10997 ax-resscn 10998 ax-1cn 10999 ax-icn 11000 ax-addcl 11001 ax-addrcl 11002 ax-mulcl 11003 ax-mulrcl 11004 ax-mulcom 11005 ax-addass 11006 ax-mulass 11007 ax-distr 11008 ax-i2m1 11009 ax-1ne0 11010 ax-1rid 11011 ax-rnegex 11012 ax-rrecex 11013 ax-cnre 11014 ax-pre-lttri 11015 ax-pre-lttrn 11016 ax-pre-ltadd 11017 ax-pre-mulgt0 11018 ax-pre-sup 11019 ax-addf 11020 ax-mulf 11021 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3443 df-sbc 3726 df-csb 3842 df-dif 3899 df-un 3901 df-in 3903 df-ss 3913 df-pss 3915 df-symdif 4186 df-nul 4267 df-if 4470 df-pw 4545 df-sn 4570 df-pr 4572 df-tp 4574 df-op 4576 df-uni 4849 df-int 4891 df-iun 4937 df-iin 4938 df-disj 5051 df-br 5086 df-opab 5148 df-mpt 5169 df-tr 5203 df-id 5505 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5560 df-se 5561 df-we 5562 df-xp 5611 df-rel 5612 df-cnv 5613 df-co 5614 df-dm 5615 df-rn 5616 df-res 5617 df-ima 5618 df-pred 6222 df-ord 6289 df-on 6290 df-lim 6291 df-suc 6292 df-iota 6415 df-fun 6465 df-fn 6466 df-f 6467 df-f1 6468 df-fo 6469 df-f1o 6470 df-fv 6471 df-isom 6472 df-riota 7270 df-ov 7316 df-oprab 7317 df-mpo 7318 df-of 7571 df-ofr 7572 df-om 7756 df-1st 7874 df-2nd 7875 df-supp 8023 df-frecs 8142 df-wrecs 8173 df-recs 8247 df-rdg 8286 df-1o 8342 df-2o 8343 df-oadd 8346 df-omul 8347 df-er 8544 df-map 8663 df-pm 8664 df-ixp 8732 df-en 8780 df-dom 8781 df-sdom 8782 df-fin 8783 df-fsupp 9197 df-fi 9238 df-sup 9269 df-inf 9270 df-oi 9337 df-dju 9727 df-card 9765 df-acn 9768 df-pnf 11081 df-mnf 11082 df-xr 11083 df-ltxr 11084 df-le 11085 df-sub 11277 df-neg 11278 df-div 11703 df-nn 12044 df-2 12106 df-3 12107 df-4 12108 df-5 12109 df-6 12110 df-7 12111 df-8 12112 df-9 12113 df-n0 12304 df-z 12390 df-dec 12508 df-uz 12653 df-q 12759 df-rp 12801 df-xneg 12918 df-xadd 12919 df-xmul 12920 df-ioo 13153 df-ioc 13154 df-ico 13155 df-icc 13156 df-fz 13310 df-fzo 13453 df-fl 13582 df-mod 13660 df-seq 13792 df-exp 13853 df-fac 14058 df-bc 14087 df-hash 14115 df-shft 14847 df-cj 14879 df-re 14880 df-im 14881 df-sqrt 15015 df-abs 15016 df-limsup 15249 df-clim 15266 df-rlim 15267 df-sum 15467 df-prod 15685 df-ef 15846 df-sin 15848 df-cos 15849 df-pi 15851 df-struct 16915 df-sets 16932 df-slot 16950 df-ndx 16962 df-base 16980 df-ress 17009 df-plusg 17042 df-mulr 17043 df-starv 17044 df-sca 17045 df-vsca 17046 df-ip 17047 df-tset 17048 df-ple 17049 df-ds 17051 df-unif 17052 df-hom 17053 df-cco 17054 df-rest 17200 df-topn 17201 df-0g 17219 df-gsum 17220 df-topgen 17221 df-pt 17222 df-prds 17225 df-xrs 17280 df-qtop 17285 df-imas 17286 df-xps 17288 df-mre 17362 df-mrc 17363 df-acs 17365 df-mgm 18393 df-sgrp 18442 df-mnd 18453 df-submnd 18498 df-mulg 18768 df-cntz 18990 df-cmn 19455 df-psmet 20660 df-xmet 20661 df-met 20662 df-bl 20663 df-mopn 20664 df-fbas 20665 df-fg 20666 df-cnfld 20669 df-top 22114 df-topon 22131 df-topsp 22153 df-bases 22167 df-cld 22241 df-ntr 22242 df-cls 22243 df-nei 22320 df-lp 22358 df-perf 22359 df-cn 22449 df-cnp 22450 df-haus 22537 df-cmp 22609 df-tx 22784 df-hmeo 22977 df-fil 23068 df-fm 23160 df-flim 23161 df-flf 23162 df-xms 23544 df-ms 23545 df-tms 23546 df-cncf 24112 df-ovol 24699 df-vol 24700 df-mbf 24854 df-itg1 24855 df-itg2 24856 df-ibl 24857 df-itg 24858 df-0p 24905 df-limc 25101 df-dv 25102 df-ind 32085 df-repr 32695 df-vts 32722 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |