logdivsum

Description: Asymptotic analysis of sum_ n <_ x , log n / n = ( log x ) ^ 2 / 2 + L + O ( log x / x ) . (Contributed by Mario Carneiro, 18-May-2016)

		Ref	Expression
	Hypothesis	logdivsum.1	$⊢ F = (y \in ℝ^{+} ⟼ \sum_{i = 1}^{⌊y⌋} (\frac{\log i}{i}) - (\frac{{\log y}^{2}}{2}))$
	Assertion	logdivsum	$⊢ (F : ℝ^{+} ⟶ ℝ \land F \in dom \underset{ℝ}{⇝} \land ((F \underset{ℝ}{⇝} L \land A \in ℝ^{+} \land e \leq A) \to \|F (A) - L\| \leq \frac{\log A}{A}))$

Proof

Step	Hyp	Ref	Expression
1		logdivsum.1	$⊢ F = (y \in ℝ^{+} ⟼ \sum_{i = 1}^{⌊y⌋} (\frac{\log i}{i}) - (\frac{{\log y}^{2}}{2}))$
2		ioorp	$⊢ (0, +∞) = ℝ^{+}$
3	2	eqcomi	$⊢ ℝ^{+} = (0, +∞)$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ ⊤ \to 1 \in ℤ$
6		ere	$⊢ e \in ℝ$
7	6	a1i	$⊢ ⊤ \to e \in ℝ$
8		0re	$⊢ 0 \in ℝ$
9		epos	$⊢ 0 < e$
10	8 6 9	ltleii	$⊢ 0 \leq e$
11	10	a1i	$⊢ ⊤ \to 0 \leq e$
12		1re	$⊢ 1 \in ℝ$
13		addge02	$⊢ (1 \in ℝ \land e \in ℝ) \to (0 \leq e \leftrightarrow 1 \leq e + 1)$
14	12 6 13	mp2an	$⊢ 0 \leq e \leftrightarrow 1 \leq e + 1$
15	11 14	sylib	$⊢ ⊤ \to 1 \leq e + 1$
16	8	a1i	$⊢ ⊤ \to 0 \in ℝ$
17		relogcl	$⊢ y \in ℝ^{+} \to \log y \in ℝ$
18	17	adantl	$⊢ (⊤ \land y \in ℝ^{+}) \to \log y \in ℝ$
19	18	resqcld	$⊢ (⊤ \land y \in ℝ^{+}) \to {\log y}^{2} \in ℝ$
20	19	rehalfcld	$⊢ (⊤ \land y \in ℝ^{+}) \to \frac{{\log y}^{2}}{2} \in ℝ$
21		rerpdivcl	$⊢ (\log y \in ℝ \land y \in ℝ^{+}) \to \frac{\log y}{y} \in ℝ$
22	17 21	mpancom	$⊢ y \in ℝ^{+} \to \frac{\log y}{y} \in ℝ$
23	22	adantl	$⊢ (⊤ \land y \in ℝ^{+}) \to \frac{\log y}{y} \in ℝ$
24		nnrp	$⊢ y \in ℕ \to y \in ℝ^{+}$
25	24 23	sylan2	$⊢ (⊤ \land y \in ℕ) \to \frac{\log y}{y} \in ℝ$
26		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
27	26	a1i	$⊢ ⊤ \to ℝ \in \{ℝ, ℂ\}$
28		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
29	28	a1i	$⊢ ⊤ \to ℂ \in \{ℝ, ℂ\}$
30	18	recnd	$⊢ (⊤ \land y \in ℝ^{+}) \to \log y \in ℂ$
31		ovexd	$⊢ (⊤ \land y \in ℝ^{+}) \to \frac{1}{y} \in V$
32		sqcl	$⊢ x \in ℂ \to x^{2} \in ℂ$
33	32	adantl	$⊢ (⊤ \land x \in ℂ) \to x^{2} \in ℂ$
34	33	halfcld	$⊢ (⊤ \land x \in ℂ) \to \frac{x^{2}}{2} \in ℂ$
35		simpr	$⊢ (⊤ \land x \in ℂ) \to x \in ℂ$
36		dvrelog	$⊢ ℝ D ({log ↾}_{ℝ^{+}}) = (y \in ℝ^{+} ⟼ \frac{1}{y})$
37		relogf1o	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ$
38		f1of	$⊢ ({log ↾}_{ℝ^{+}}) : ℝ^{+} \underset{1-1 onto}{⟶} ℝ \to ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
39	37 38	mp1i	$⊢ ⊤ \to ({log ↾}_{ℝ^{+}}) : ℝ^{+} ⟶ ℝ$
40	39	feqmptd	$⊢ ⊤ \to {log ↾}_{ℝ^{+}} = (y \in ℝ^{+} ⟼ ({log ↾}_{ℝ^{+}}) (y))$
41		fvres	$⊢ y \in ℝ^{+} \to ({log ↾}_{ℝ^{+}}) (y) = \log y$
42	41	mpteq2ia	$⊢ (y \in ℝ^{+} ⟼ ({log ↾}_{ℝ^{+}}) (y)) = (y \in ℝ^{+} ⟼ \log y)$
43	40 42	eqtrdi	$⊢ ⊤ \to {log ↾}_{ℝ^{+}} = (y \in ℝ^{+} ⟼ \log y)$
44	43	oveq2d	$⊢ ⊤ \to ℝ D ({log ↾}_{ℝ^{+}}) = \frac{d (y \in ℝ^{+}⟼ \log y)}{d_{ℝ} y}$
45	36 44	syl5reqr	$⊢ ⊤ \to \frac{d (y \in ℝ^{+}⟼ \log y)}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \frac{1}{y})$
46		ovexd	$⊢ (⊤ \land x \in ℂ) \to 2 x \in V$
47		2nn	$⊢ 2 \in ℕ$
48		dvexp	$⊢ 2 \in ℕ \to \frac{d (x \in ℂ⟼ x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 2 x^{2 - 1})$
49	47 48	mp1i	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 2 x^{2 - 1})$
50		2m1e1	$⊢ 2 - 1 = 1$
51	50	oveq2i	$⊢ x^{2 - 1} = x^{1}$
52		exp1	$⊢ x \in ℂ \to x^{1} = x$
53	52	adantl	$⊢ (⊤ \land x \in ℂ) \to x^{1} = x$
54	51 53	syl5eq	$⊢ (⊤ \land x \in ℂ) \to x^{2 - 1} = x$
55	54	oveq2d	$⊢ (⊤ \land x \in ℂ) \to 2 x^{2 - 1} = 2 x$
56	55	mpteq2dva	$⊢ ⊤ \to (x \in ℂ ⟼ 2 x^{2 - 1}) = (x \in ℂ ⟼ 2 x)$
57	49 56	eqtrd	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ x^{2})}{d_{ℂ} x} = (x \in ℂ ⟼ 2 x)$
58		2cnd	$⊢ ⊤ \to 2 \in ℂ$
59		2ne0	$⊢ 2 \neq 0$
60	59	a1i	$⊢ ⊤ \to 2 \neq 0$
61	29 33 46 57 58 60	dvmptdivc	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ \frac{x^{2}}{2})}{d_{ℂ} x} = (x \in ℂ ⟼ \frac{2 x}{2})$
62		2cn	$⊢ 2 \in ℂ$
63		divcan3	$⊢ (x \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 x}{2} = x$
64	62 59 63	mp3an23	$⊢ x \in ℂ \to \frac{2 x}{2} = x$
65	64	adantl	$⊢ (⊤ \land x \in ℂ) \to \frac{2 x}{2} = x$
66	65	mpteq2dva	$⊢ ⊤ \to (x \in ℂ ⟼ \frac{2 x}{2}) = (x \in ℂ ⟼ x)$
67	61 66	eqtrd	$⊢ ⊤ \to \frac{d (x \in ℂ⟼ \frac{x^{2}}{2})}{d_{ℂ} x} = (x \in ℂ ⟼ x)$
68		oveq1	$⊢ x = \log y \to x^{2} = {\log y}^{2}$
69	68	oveq1d	$⊢ x = \log y \to \frac{x^{2}}{2} = \frac{{\log y}^{2}}{2}$
70		id	$⊢ x = \log y \to x = \log y$
71	27 29 30 31 34 35 45 67 69 70	dvmptco	$⊢ ⊤ \to \frac{d (y \in ℝ^{+}⟼ \frac{{\log y}^{2}}{2})}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \log y (\frac{1}{y}))$
72		rpcn	$⊢ y \in ℝ^{+} \to y \in ℂ$
73	72	adantl	$⊢ (⊤ \land y \in ℝ^{+}) \to y \in ℂ$
74		rpne0	$⊢ y \in ℝ^{+} \to y \neq 0$
75	74	adantl	$⊢ (⊤ \land y \in ℝ^{+}) \to y \neq 0$
76	30 73 75	divrecd	$⊢ (⊤ \land y \in ℝ^{+}) \to \frac{\log y}{y} = \log y (\frac{1}{y})$
77	76	mpteq2dva	$⊢ ⊤ \to (y \in ℝ^{+} ⟼ \frac{\log y}{y}) = (y \in ℝ^{+} ⟼ \log y (\frac{1}{y}))$
78	71 77	eqtr4d	$⊢ ⊤ \to \frac{d (y \in ℝ^{+}⟼ \frac{{\log y}^{2}}{2})}{d_{ℝ} y} = (y \in ℝ^{+} ⟼ \frac{\log y}{y})$
79		fveq2	$⊢ y = i \to \log y = \log i$
80		id	$⊢ y = i \to y = i$
81	79 80	oveq12d	$⊢ y = i \to \frac{\log y}{y} = \frac{\log i}{i}$
82		simp3r	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to y \leq i$
83		simp2l	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to y \in ℝ^{+}$
84	83	rpred	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to y \in ℝ$
85		simp3l	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to e \leq y$
86		simp2r	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to i \in ℝ^{+}$
87	86	rpred	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to i \in ℝ$
88	6	a1i	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to e \in ℝ$
89	88 84 87 85 82	letrd	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to e \leq i$
90		logdivle	$⊢ ((y \in ℝ \land e \leq y) \land (i \in ℝ \land e \leq i)) \to (y \leq i \leftrightarrow \frac{\log i}{i} \leq \frac{\log y}{y})$
91	84 85 87 89 90	syl22anc	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to (y \leq i \leftrightarrow \frac{\log i}{i} \leq \frac{\log y}{y})$
92	82 91	mpbid	$⊢ (⊤ \land (y \in ℝ^{+} \land i \in ℝ^{+}) \land (e \leq y \land y \leq i)) \to \frac{\log i}{i} \leq \frac{\log y}{y}$
93	72	cxp1d	$⊢ y \in ℝ^{+} \to y^{1} = y$
94	93	oveq2d	$⊢ y \in ℝ^{+} \to \frac{\log y}{y^{1}} = \frac{\log y}{y}$
95	94	mpteq2ia	$⊢ (y \in ℝ^{+} ⟼ \frac{\log y}{y^{1}}) = (y \in ℝ^{+} ⟼ \frac{\log y}{y})$
96		1rp	$⊢ 1 \in ℝ^{+}$
97		cxploglim	$⊢ 1 \in ℝ^{+} \to (y \in ℝ^{+} ⟼ \frac{\log y}{y^{1}}) \underset{ℝ}{⇝} 0$
98	96 97	mp1i	$⊢ ⊤ \to (y \in ℝ^{+} ⟼ \frac{\log y}{y^{1}}) \underset{ℝ}{⇝} 0$
99	95 98	eqbrtrrid	$⊢ ⊤ \to (y \in ℝ^{+} ⟼ \frac{\log y}{y}) \underset{ℝ}{⇝} 0$
100		fveq2	$⊢ y = A \to \log y = \log A$
101		id	$⊢ y = A \to y = A$
102	100 101	oveq12d	$⊢ y = A \to \frac{\log y}{y} = \frac{\log A}{A}$
103	3 4 5 7 15 16 20 23 25 78 81 92 1 99 102	dvfsumrlim3	$⊢ ⊤ \to (F : ℝ^{+} ⟶ ℝ \land F \in dom \underset{ℝ}{⇝} \land ((F \underset{ℝ}{⇝} L \land A \in ℝ^{+} \land e \leq A) \to \|F (A) - L\| \leq \frac{\log A}{A}))$
104	103	mptru	$⊢ (F : ℝ^{+} ⟶ ℝ \land F \in dom \underset{ℝ}{⇝} \land ((F \underset{ℝ}{⇝} L \land A \in ℝ^{+} \land e \leq A) \to \|F (A) - L\| \leq \frac{\log A}{A}))$

Metamath Proof Explorer

Theorem logdivsum

Proof