circlemethnat - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > circlemethnat		Structured version Visualization version GIF version

Theorem circlemethnat 31053

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.)

**Hypotheses**
Ref	Expression
circlemethnat.r	⊢ 𝑅 = (♯‘(𝐴(repr‘𝑆)𝑁))
circlemethnat.f	⊢ 𝐹 = ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥)
circlemethnat.n	⊢ 𝑁 ∈ ℕ₀
circlemethnat.a	⊢ 𝐴 ⊆ ℕ
circlemethnat.s	⊢ 𝑆 ∈ ℕ

**Assertion**
Ref	Expression
circlemethnat	⊢ 𝑅 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥

Distinct variable groups: 𝑥,𝐴 𝑥,𝑁 𝑥,𝑆 Allowed substitution hints: 𝑅(𝑥) 𝐹(𝑥)

Proof of Theorem circlemethnat Dummy variables 𝑎 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnex 11227	. . . . . . . . . . . . . 14 ⊢ ℕ ∈ V
2		circlemethnat.a	. . . . . . . . . . . . . 14 ⊢ 𝐴 ⊆ ℕ
3		indf 30411	. . . . . . . . . . . . . 14 ⊢ ((ℕ ∈ V ∧ 𝐴 ⊆ ℕ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1})
4	1, 2, 3	mp2an 664	. . . . . . . . . . . . 13 ⊢ ((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}
5		pr01ssre 29904	. . . . . . . . . . . . . 14 ⊢ {0, 1} ⊆ ℝ
6		ax-resscn 10194	. . . . . . . . . . . . . 14 ⊢ ℝ ⊆ ℂ
7	5, 6	sstri 3759	. . . . . . . . . . . . 13 ⊢ {0, 1} ⊆ ℂ
8		fss 6196	. . . . . . . . . . . . 13 ⊢ ((((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆ ℂ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ)
9	4, 7, 8	mp2an 664	. . . . . . . . . . . 12 ⊢ ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ
10		cnex 10218	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
11	10, 1	elmap 8037	. . . . . . . . . . . 12 ⊢ (((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑_𝑚 ℕ) ↔ ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ)
12	9, 11	mpbir 221	. . . . . . . . . . 11 ⊢ ((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑_𝑚 ℕ)
13	12	elexi 3362	. . . . . . . . . 10 ⊢ ((𝟭‘ℕ)‘𝐴) ∈ V
14	13	fvconst2 6612	. . . . . . . . 9 ⊢ (𝑎 ∈ (0..^𝑆) → (((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴))
15	14	adantl 467	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑐 ∈ (ℕ(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → (((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴))
16	15	fveq1d 6334	. . . . . . 7 ⊢ (((⊤ ∧ 𝑐 ∈ (ℕ(repr‘𝑆)𝑁)) ∧ 𝑎 ∈ (0..^𝑆)) → ((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)))
17	16	prodeq2dv 14859	. . . . . 6 ⊢ ((⊤ ∧ 𝑐 ∈ (ℕ(repr‘𝑆)𝑁)) → ∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)))
18	17	sumeq2dv 14640	. . . . 5 ⊢ (⊤ → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)))
19	2	a1i 11	. . . . . 6 ⊢ (⊤ → 𝐴 ⊆ ℕ)
20		circlemethnat.n	. . . . . . 7 ⊢ 𝑁 ∈ ℕ₀
21	20	a1i 11	. . . . . 6 ⊢ (⊤ → 𝑁 ∈ ℕ₀)
22		circlemethnat.s	. . . . . . . 8 ⊢ 𝑆 ∈ ℕ
23	22	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝑆 ∈ ℕ)
24	23	nnnn0d 11552	. . . . . 6 ⊢ (⊤ → 𝑆 ∈ ℕ₀)
25	19, 21, 24	hashrepr 31037	. . . . 5 ⊢ (⊤ → (♯‘(𝐴(repr‘𝑆)𝑁)) = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)))
26	18, 25	eqtr4d 2807	. . . 4 ⊢ (⊤ → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (♯‘(𝐴(repr‘𝑆)𝑁)))
27		circlemethnat.r	. . . 4 ⊢ 𝑅 = (♯‘(𝐴(repr‘𝑆)𝑁))
28	26, 27	syl6reqr 2823	. . 3 ⊢ (⊤ → 𝑅 = Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)))
29	12	fconst6 6235	. . . . 5 ⊢ ((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑_𝑚 ℕ)
30	29	a1i 11	. . . 4 ⊢ (⊤ → ((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑_𝑚 ℕ))
31	21, 23, 30	circlemeth 31052	. . 3 ⊢ (⊤ → Σ𝑐 ∈ (ℕ(repr‘𝑆)𝑁)∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
32		fzofi 12980	. . . . . . . 8 ⊢ (0..^𝑆) ∈ Fin
33	32	a1i 11	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (0..^𝑆) ∈ Fin)
34		circlemethnat.f	. . . . . . . 8 ⊢ 𝐹 = ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥)
35	20	a1i 11	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝑁 ∈ ℕ₀)
36		ioossre 12439	. . . . . . . . . . . 12 ⊢ (0(,)1) ⊆ ℝ
37	36, 6	sstri 3759	. . . . . . . . . . 11 ⊢ (0(,)1) ⊆ ℂ
38	37	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → (0(,)1) ⊆ ℂ)
39	38	sselda 3750	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝑥 ∈ ℂ)
40	9	a1i 11	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ)
41	35, 39, 40	vtscl 31050	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥) ∈ ℂ)
42	34, 41	syl5eqel 2853	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝐹 ∈ ℂ)
43		fprodconst 14914	. . . . . . 7 ⊢ (((0..^𝑆) ∈ Fin ∧ 𝐹 ∈ ℂ) → ∏𝑎 ∈ (0..^𝑆)𝐹 = (𝐹↑(♯‘(0..^𝑆))))
44	33, 42, 43	syl2anc 565	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)𝐹 = (𝐹↑(♯‘(0..^𝑆))))
45	14	adantl 467	. . . . . . . . . 10 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → (((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴))
46	45	oveq1d 6807	. . . . . . . . 9 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → ((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁) = (((𝟭‘ℕ)‘𝐴)vts𝑁))
47	46	fveq1d 6334	. . . . . . . 8 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → (((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) = ((((𝟭‘ℕ)‘𝐴)vts𝑁)‘𝑥))
48	47, 34	syl6reqr 2823	. . . . . . 7 ⊢ (((⊤ ∧ 𝑥 ∈ (0(,)1)) ∧ 𝑎 ∈ (0..^𝑆)) → 𝐹 = (((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥))
49	48	prodeq2dv 14859	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)𝐹 = ∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥))
50	24	adantr 466	. . . . . . . 8 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → 𝑆 ∈ ℕ₀)
51		hashfzo0 13418	. . . . . . . 8 ⊢ (𝑆 ∈ ℕ₀ → (♯‘(0..^𝑆)) = 𝑆)
52	50, 51	syl 17	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (♯‘(0..^𝑆)) = 𝑆)
53	52	oveq2d 6808	. . . . . 6 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (𝐹↑(♯‘(0..^𝑆))) = (𝐹↑𝑆))
54	44, 49, 53	3eqtr3d 2812	. . . . 5 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → ∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) = (𝐹↑𝑆))
55	54	oveq1d 6807	. . . 4 ⊢ ((⊤ ∧ 𝑥 ∈ (0(,)1)) → (∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) = ((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))))
56	55	itgeq2dv 23767	. . 3 ⊢ (⊤ → ∫(0(,)1)(∏𝑎 ∈ (0..^𝑆)(((((0..^𝑆) × {((𝟭‘ℕ)‘𝐴)})‘𝑎)vts𝑁)‘𝑥) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
57	28, 31, 56	3eqtrd 2808	. 2 ⊢ (⊤ → 𝑅 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥)
58	57	trud 1640	1 ⊢ 𝑅 = ∫(0(,)1)((𝐹↑𝑆) · (exp‘((i · (2 · π)) · (-𝑁 · 𝑥)))) d𝑥

Colors of variables: wff setvar class

Syntax hints: ∧ wa 382 = wceq 1630 ⊤wtru 1631 ∈ wcel 2144 Vcvv 3349 ⊆ wss 3721 {csn 4314 {cpr 4316 × cxp 5247 ⟶wf 6027 ‘cfv 6031 (class class class)co 6792 ↑_𝑚 cmap 8008 Fincfn 8108 ℂcc 10135 ℝcr 10136 0cc0 10137 1c1 10138 ici 10139 · cmul 10142 -cneg 10468 ℕcn 11221 2c2 11271 ℕ₀cn0 11493 (,)cioo 12379 ..^cfzo 12672 ↑cexp 13066 ♯chash 13320 Σcsu 14623 ∏cprod 14841 expce 14997 πcpi 15002 ∫citg 23605 𝟭cind 30406 reprcrepr 31020 vtscvts 31047

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-8 2146 ax-9 2153 ax-10 2173 ax-11 2189 ax-12 2202 ax-13 2407 ax-ext 2750 ax-rep 4902 ax-sep 4912 ax-nul 4920 ax-pow 4971 ax-pr 5034 ax-un 7095 ax-inf2 8701 ax-cc 9458 ax-cnex 10193 ax-resscn 10194 ax-1cn 10195 ax-icn 10196 ax-addcl 10197 ax-addrcl 10198 ax-mulcl 10199 ax-mulrcl 10200 ax-mulcom 10201 ax-addass 10202 ax-mulass 10203 ax-distr 10204 ax-i2m1 10205 ax-1ne0 10206 ax-1rid 10207 ax-rnegex 10208 ax-rrecex 10209 ax-cnre 10210 ax-pre-lttri 10211 ax-pre-lttrn 10212 ax-pre-ltadd 10213 ax-pre-mulgt0 10214 ax-pre-sup 10215 ax-addf 10216 ax-mulf 10217

This theorem depends on definitions: df-bi 197 df-an 383 df-or 827 df-3or 1071 df-3an 1072 df-tru 1633 df-fal 1636 df-ex 1852 df-nf 1857 df-sb 2049 df-eu 2621 df-mo 2622 df-clab 2757 df-cleq 2763 df-clel 2766 df-nfc 2901 df-ne 2943 df-nel 3046 df-ral 3065 df-rex 3066 df-reu 3067 df-rmo 3068 df-rab 3069 df-v 3351 df-sbc 3586 df-csb 3681 df-dif 3724 df-un 3726 df-in 3728 df-ss 3735 df-pss 3737 df-nul 4062 df-if 4224 df-pw 4297 df-sn 4315 df-pr 4317 df-tp 4319 df-op 4321 df-uni 4573 df-int 4610 df-iun 4654 df-iin 4655 df-disj 4753 df-br 4785 df-opab 4845 df-mpt 4862 df-tr 4885 df-id 5157 df-eprel 5162 df-po 5170 df-so 5171 df-fr 5208 df-se 5209 df-we 5210 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-rn 5260 df-res 5261 df-ima 5262 df-pred 5823 df-ord 5869 df-on 5870 df-lim 5871 df-suc 5872 df-iota 5994 df-fun 6033 df-fn 6034 df-f 6035 df-f1 6036 df-fo 6037 df-f1o 6038 df-fv 6039 df-isom 6040 df-riota 6753 df-ov 6795 df-oprab 6796 df-mpt2 6797 df-of 7043 df-ofr 7044 df-om 7212 df-1st 7314 df-2nd 7315 df-supp 7446 df-wrecs 7558 df-recs 7620 df-rdg 7658 df-1o 7712 df-2o 7713 df-oadd 7716 df-omul 7717 df-er 7895 df-map 8010 df-pm 8011 df-ixp 8062 df-en 8109 df-dom 8110 df-sdom 8111 df-fin 8112 df-fsupp 8431 df-fi 8472 df-sup 8503 df-inf 8504 df-oi 8570 df-card 8964 df-acn 8967 df-cda 9191 df-pnf 10277 df-mnf 10278 df-xr 10279 df-ltxr 10280 df-le 10281 df-sub 10469 df-neg 10470 df-div 10886 df-nn 11222 df-2 11280 df-3 11281 df-4 11282 df-5 11283 df-6 11284 df-7 11285 df-8 11286 df-9 11287 df-n0 11494 df-z 11579 df-dec 11695 df-uz 11888 df-q 11991 df-rp 12035 df-xneg 12150 df-xadd 12151 df-xmul 12152 df-ioo 12383 df-ioc 12384 df-ico 12385 df-icc 12386 df-fz 12533 df-fzo 12673 df-fl 12800 df-mod 12876 df-seq 13008 df-exp 13067 df-fac 13264 df-bc 13293 df-hash 13321 df-shft 14014 df-cj 14046 df-re 14047 df-im 14048 df-sqrt 14182 df-abs 14183 df-limsup 14409 df-clim 14426 df-rlim 14427 df-sum 14624 df-prod 14842 df-ef 15003 df-sin 15005 df-cos 15006 df-pi 15008 df-struct 16065 df-ndx 16066 df-slot 16067 df-base 16069 df-sets 16070 df-ress 16071 df-plusg 16161 df-mulr 16162 df-starv 16163 df-sca 16164 df-vsca 16165 df-ip 16166 df-tset 16167 df-ple 16168 df-ds 16171 df-unif 16172 df-hom 16173 df-cco 16174 df-rest 16290 df-topn 16291 df-0g 16309 df-gsum 16310 df-topgen 16311 df-pt 16312 df-prds 16315 df-xrs 16369 df-qtop 16374 df-imas 16375 df-xps 16377 df-mre 16453 df-mrc 16454 df-acs 16456 df-mgm 17449 df-sgrp 17491 df-mnd 17502 df-submnd 17543 df-mulg 17748 df-cntz 17956 df-cmn 18401 df-psmet 19952 df-xmet 19953 df-met 19954 df-bl 19955 df-mopn 19956 df-fbas 19957 df-fg 19958 df-cnfld 19961 df-top 20918 df-topon 20935 df-topsp 20957 df-bases 20970 df-cld 21043 df-ntr 21044 df-cls 21045 df-nei 21122 df-lp 21160 df-perf 21161 df-cn 21251 df-cnp 21252 df-haus 21339 df-cmp 21410 df-tx 21585 df-hmeo 21778 df-fil 21869 df-fm 21961 df-flim 21962 df-flf 21963 df-xms 22344 df-ms 22345 df-tms 22346 df-cncf 22900 df-ovol 23451 df-vol 23452 df-mbf 23606 df-itg1 23607 df-itg2 23608 df-ibl 23609 df-itg 23610 df-0p 23656 df-limc 23849 df-dv 23850 df-ind 30407 df-repr 31021 df-vts 31048

This theorem is referenced by: (None)

W3C validator