selberg

Description: Selberg's symmetry formula. The statement has many forms, and this one is equivalent to the statement that sum_ n <_ x , Lam ( n ) log n + sum_ m x. n <_ x , Lam ( m ) Lam ( n ) = 2 x log x + O ( x ) . Equation 10.4.10 of Shapiro, p. 419. (Contributed by Mario Carneiro, 23-May-2016)

		Ref	Expression
	Assertion	selberg	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ n = d \to Λ (n) = Λ (d)$
2		oveq2	$⊢ n = d \to \frac{x}{n} = \frac{x}{d}$
3	2	fveq2d	$⊢ n = d \to ψ (\frac{x}{n}) = ψ (\frac{x}{d})$
4	1 3	oveq12d	$⊢ n = d \to Λ (n) ψ (\frac{x}{n}) = Λ (d) ψ (\frac{x}{d})$
5	4	cbvsumv	$⊢ \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) = \sum_{d = 1}^{⌊x⌋} Λ (d) ψ (\frac{x}{d})$
6		fzfid	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to (1 \dots ⌊\frac{x}{d}⌋) \in Fin$
7		elfznn	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℕ$
8	7	adantl	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to d \in ℕ$
9		vmacl	$⊢ d \in ℕ \to Λ (d) \in ℝ$
10	8 9	syl	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to Λ (d) \in ℝ$
11	10	recnd	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to Λ (d) \in ℂ$
12		elfznn	$⊢ m \in (1 \dots ⌊\frac{x}{d}⌋) \to m \in ℕ$
13	12	adantl	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \in ℕ$
14		vmacl	$⊢ m \in ℕ \to Λ (m) \in ℝ$
15	13 14	syl	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to Λ (m) \in ℝ$
16	15	recnd	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to Λ (m) \in ℂ$
17	6 11 16	fsummulc2	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to Λ (d) \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (m) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (d) Λ (m)$
18	7	nnrpd	$⊢ d \in (1 \dots ⌊x⌋) \to d \in ℝ^{+}$
19		rpdivcl	$⊢ (x \in ℝ^{+} \land d \in ℝ^{+}) \to \frac{x}{d} \in ℝ^{+}$
20	18 19	sylan2	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in ℝ^{+}$
21	20	rpred	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to \frac{x}{d} \in ℝ$
22		chpval	$⊢ \frac{x}{d} \in ℝ \to ψ (\frac{x}{d}) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (m)$
23	21 22	syl	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{d}) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (m)$
24	23	oveq2d	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to Λ (d) ψ (\frac{x}{d}) = Λ (d) \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (m)$
25	13	nncnd	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to m \in ℂ$
26	7	ad2antlr	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \in ℕ$
27	26	nncnd	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \in ℂ$
28	26	nnne0d	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to d \neq 0$
29	25 27 28	divcan3d	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \frac{d m}{d} = m$
30	29	fveq2d	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to Λ (\frac{d m}{d}) = Λ (m)$
31	30	oveq2d	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to Λ (d) Λ (\frac{d m}{d}) = Λ (d) Λ (m)$
32	31	sumeq2dv	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (d) Λ (\frac{d m}{d}) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (d) Λ (m)$
33	17 24 32	3eqtr4d	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to Λ (d) ψ (\frac{x}{d}) = \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (d) Λ (\frac{d m}{d})$
34	33	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{d = 1}^{⌊x⌋} Λ (d) ψ (\frac{x}{d}) = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (d) Λ (\frac{d m}{d})$
35	5 34	syl5eq	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (d) Λ (\frac{d m}{d})$
36		fvoveq1	$⊢ n = d m \to Λ (\frac{n}{d}) = Λ (\frac{d m}{d})$
37	36	oveq2d	$⊢ n = d m \to Λ (d) Λ (\frac{n}{d}) = Λ (d) Λ (\frac{d m}{d})$
38		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
39		ssrab2	$⊢ \{y \in ℕ \| y ∥ n\} \subseteq ℕ$
40		simprr	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to d \in \{y \in ℕ \| y ∥ n\}$
41	39 40	sseldi	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to d \in ℕ$
42	41	anassrs	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land d \in \{y \in ℕ \| y ∥ n\}) \to d \in ℕ$
43	42 9	syl	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land d \in \{y \in ℕ \| y ∥ n\}) \to Λ (d) \in ℝ$
44		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
45	44	adantl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
46		dvdsdivcl	$⊢ (n \in ℕ \land d \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{d} \in \{y \in ℕ \| y ∥ n\}$
47	45 46	sylan	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land d \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{d} \in \{y \in ℕ \| y ∥ n\}$
48	39 47	sseldi	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land d \in \{y \in ℕ \| y ∥ n\}) \to \frac{n}{d} \in ℕ$
49		vmacl	$⊢ \frac{n}{d} \in ℕ \to Λ (\frac{n}{d}) \in ℝ$
50	48 49	syl	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land d \in \{y \in ℕ \| y ∥ n\}) \to Λ (\frac{n}{d}) \in ℝ$
51	43 50	remulcld	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land d \in \{y \in ℕ \| y ∥ n\}) \to Λ (d) Λ (\frac{n}{d}) \in ℝ$
52	51	recnd	$⊢ ((x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \land d \in \{y \in ℕ \| y ∥ n\}) \to Λ (d) Λ (\frac{n}{d}) \in ℂ$
53	52	anasss	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to Λ (d) Λ (\frac{n}{d}) \in ℂ$
54	37 38 53	dvdsflsumcom	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} Λ (d) Λ (\frac{d m}{d})$
55	35 54	eqtr4d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) = \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d})$
56	55	oveq1d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + \sum_{n = 1}^{⌊x⌋} Λ (n) \log n = \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) + \sum_{n = 1}^{⌊x⌋} Λ (n) \log n$
57		fzfid	$⊢ x \in ℝ^{+} \to (1 \dots ⌊x⌋) \in Fin$
58		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
59	45 58	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℝ$
60	59	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \in ℂ$
61	44	nnrpd	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℝ^{+}$
62		rpdivcl	$⊢ (x \in ℝ^{+} \land n \in ℝ^{+}) \to \frac{x}{n} \in ℝ^{+}$
63	61 62	sylan2	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ^{+}$
64	63	rpred	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \frac{x}{n} \in ℝ$
65		chpcl	$⊢ \frac{x}{n} \in ℝ \to ψ (\frac{x}{n}) \in ℝ$
66	64 65	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℝ$
67	66	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to ψ (\frac{x}{n}) \in ℂ$
68	60 67	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) ψ (\frac{x}{n}) \in ℂ$
69	45	nnrpd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to n \in ℝ^{+}$
70		relogcl	$⊢ n \in ℝ^{+} \to \log n \in ℝ$
71	69 70	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℝ$
72	71	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n \in ℂ$
73	60 72	mulcld	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) \log n \in ℂ$
74	57 68 73	fsumadd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (Λ (n) ψ (\frac{x}{n}) + Λ (n) \log n) = \sum_{n = 1}^{⌊x⌋} Λ (n) ψ (\frac{x}{n}) + \sum_{n = 1}^{⌊x⌋} Λ (n) \log n$
75		fzfid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to (1 \dots n) \in Fin$
76		dvdsssfz1	$⊢ n \in ℕ \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
77	45 76	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ n\} \subseteq (1 \dots n)$
78	75 77	ssfid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \{y \in ℕ \| y ∥ n\} \in Fin$
79	78 51	fsumrecl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) \in ℝ$
80	79	recnd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) \in ℂ$
81	57 80 73	fsumadd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (\sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) + Λ (n) \log n) = \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) + \sum_{n = 1}^{⌊x⌋} Λ (n) \log n$
82	56 74 81	3eqtr4d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} (Λ (n) ψ (\frac{x}{n}) + Λ (n) \log n) = \sum_{n = 1}^{⌊x⌋} (\sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) + Λ (n) \log n)$
83	72 67	addcomd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \log n + ψ (\frac{x}{n}) = ψ (\frac{x}{n}) + \log n$
84	83	oveq2d	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\log n + ψ (\frac{x}{n})) = Λ (n) (ψ (\frac{x}{n}) + \log n)$
85	60 67 72	adddid	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (ψ (\frac{x}{n}) + \log n) = Λ (n) ψ (\frac{x}{n}) + Λ (n) \log n$
86	84 85	eqtrd	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to Λ (n) (\log n + ψ (\frac{x}{n})) = Λ (n) ψ (\frac{x}{n}) + Λ (n) \log n$
87	86	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} (Λ (n) ψ (\frac{x}{n}) + Λ (n) \log n)$
88		logsqvma2	$⊢ n \in ℕ \to \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2} = \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) + Λ (n) \log n$
89	45 88	syl	$⊢ (x \in ℝ^{+} \land n \in (1 \dots ⌊x⌋)) \to \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2} = \sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) + Λ (n) \log n$
90	89	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2} = \sum_{n = 1}^{⌊x⌋} (\sum_{d \in \{y \in ℕ \| y ∥ n\}} Λ (d) Λ (\frac{n}{d}) + Λ (n) \log n)$
91	82 87 90	3eqtr4d	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) = \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2}$
92		fvoveq1	$⊢ n = d m \to \log (\frac{n}{d}) = \log (\frac{d m}{d})$
93	92	oveq1d	$⊢ n = d m \to {\log (\frac{n}{d})}^{2} = {\log (\frac{d m}{d})}^{2}$
94	93	oveq2d	$⊢ n = d m \to μ (d) {\log (\frac{n}{d})}^{2} = μ (d) {\log (\frac{d m}{d})}^{2}$
95		mucl	$⊢ d \in ℕ \to μ (d) \in ℤ$
96	41 95	syl	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) \in ℤ$
97	96	zcnd	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) \in ℂ$
98	61	ad2antrl	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to n \in ℝ^{+}$
99	41	nnrpd	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to d \in ℝ^{+}$
100	98 99	rpdivcld	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to \frac{n}{d} \in ℝ^{+}$
101		relogcl	$⊢ \frac{n}{d} \in ℝ^{+} \to \log (\frac{n}{d}) \in ℝ$
102	101	recnd	$⊢ \frac{n}{d} \in ℝ^{+} \to \log (\frac{n}{d}) \in ℂ$
103	100 102	syl	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to \log (\frac{n}{d}) \in ℂ$
104	103	sqcld	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to {\log (\frac{n}{d})}^{2} \in ℂ$
105	97 104	mulcld	$⊢ (x \in ℝ^{+} \land (n \in (1 \dots ⌊x⌋) \land d \in \{y \in ℕ \| y ∥ n\})) \to μ (d) {\log (\frac{n}{d})}^{2} \in ℂ$
106	94 38 105	dvdsflsumcom	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} \sum_{d \in \{y \in ℕ \| y ∥ n\}} μ (d) {\log (\frac{n}{d})}^{2} = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log (\frac{d m}{d})}^{2}$
107	29	fveq2d	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to \log (\frac{d m}{d}) = \log m$
108	107	oveq1d	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to {\log (\frac{d m}{d})}^{2} = {\log m}^{2}$
109	108	oveq2d	$⊢ ((x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \land m \in (1 \dots ⌊\frac{x}{d}⌋)) \to μ (d) {\log (\frac{d m}{d})}^{2} = μ (d) {\log m}^{2}$
110	109	sumeq2dv	$⊢ (x \in ℝ^{+} \land d \in (1 \dots ⌊x⌋)) \to \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log (\frac{d m}{d})}^{2} = \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}$
111	110	sumeq2dv	$⊢ x \in ℝ^{+} \to \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log (\frac{d m}{d})}^{2} = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}$
112	91 106 111	3eqtrd	$⊢ x \in ℝ^{+} \to \sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n})) = \sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}$
113	112	oveq1d	$⊢ x \in ℝ^{+} \to \frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x} = \frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}$
114	113	oveq1d	$⊢ x \in ℝ^{+} \to (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x = (\frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}) - 2 \log x$
115	114	mpteq2ia	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) = (x \in ℝ^{+} ⟼ (\frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}) - 2 \log x)$
116		eqid	$⊢ \frac{{\log (\frac{x}{d})}^{2} + 2 - 2 \log (\frac{x}{d})}{d} = \frac{{\log (\frac{x}{d})}^{2} + 2 - 2 \log (\frac{x}{d})}{d}$
117	116	selberglem2	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{d = 1}^{⌊x⌋} \sum_{m = 1}^{⌊\frac{x}{d}⌋} μ (d) {\log m}^{2}}{x}) - 2 \log x) \in 𝑂 (1)$
118	115 117	eqeltri	$⊢ (x \in ℝ^{+} ⟼ (\frac{\sum_{n = 1}^{⌊x⌋} Λ (n) (\log n + ψ (\frac{x}{n}))}{x}) - 2 \log x) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem selberg

Proof