dchrmusumlem

Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n , is bounded. Equation 9.4.16 of Shapiro, p. 379. (Contributed by Mario Carneiro, 12-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	dchrmusum.g	$⊢ G = DChr (N)$
	dchrmusum.d	$⊢ D = {Base}_{G}$
	dchrmusum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrmusum.b	$⊢ φ \to X \in D$
	dchrmusum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrmusum.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
	dchrmusum.c	$⊢ φ \to C \in [0, +∞)$
	dchrmusum.t	$⊢ φ \to seq 1 (+ F) ⇝ T$
	dchrmusum.2	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - T\| \leq \frac{C}{y}$
Assertion	dchrmusumlem	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n})) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		dchrmusum.g	$⊢ G = DChr (N)$
5		dchrmusum.d	$⊢ D = {Base}_{G}$
6		dchrmusum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrmusum.b	$⊢ φ \to X \in D$
8		dchrmusum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrmusum.f	$⊢ F = (a \in ℕ ⟼ \frac{X (L (a))}{a})$
10		dchrmusum.c	$⊢ φ \to C \in [0, +∞)$
11		dchrmusum.t	$⊢ φ \to seq 1 (+ F) ⇝ T$
12		dchrmusum.2	$⊢ φ \to \forall y \in [1, +∞) \|seq 1 (+ F) (⌊y⌋) - T\| \leq \frac{C}{y}$
13		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
14	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X \in D$
15		elfzelz	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℤ$
16	15	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℤ$
17	4 1 5 2 14 16	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X (L (n)) \in ℂ$
18		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
19	18	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
20		mucl	$⊢ n \in ℕ \to μ (n) \in ℤ$
21	19 20	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℤ$
22	21	zred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to μ (n) \in ℝ$
23	22 19	nndivred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℝ$
24	23	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{μ (n)}{n} \in ℂ$
25	17 24	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X (L (n)) (\frac{μ (n)}{n}) \in ℂ$
26	13 25	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) \in ℂ$
27		climcl	$⊢ seq 1 (+ F) ⇝ T \to T \in ℂ$
28	11 27	syl	$⊢ φ \to T \in ℂ$
29	28	adantr	$⊢ (φ \land x \in ℝ^{+}) \to T \in ℂ$
30	26 29	mulcld	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T \in ℂ$
31	1 2 3 4 5 6 7 8 9 10 11 12	dchrisumn0	$⊢ φ \to T \neq 0$
32	31	adantr	$⊢ (φ \land x \in ℝ^{+}) \to T \neq 0$
33	30 29 32	divrecd	$⊢ (φ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T}{T} = \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T (\frac{1}{T})$
34	26 29 32	divcan4d	$⊢ (φ \land x \in ℝ^{+}) \to \frac{\sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T}{T} = \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n})$
35	33 34	eqtr3d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T (\frac{1}{T}) = \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n})$
36	35	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T (\frac{1}{T})) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}))$
37	28 31	reccld	$⊢ φ \to \frac{1}{T} \in ℂ$
38	37	adantr	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{T} \in ℂ$
39	1 2 3 4 5 6 7 8 9 10 11 12	dchrmusum2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T) \in 𝑂 (1)$
40		rpssre	$⊢ ℝ^{+} \subseteq ℝ$
41		o1const	$⊢ (ℝ^{+} \subseteq ℝ \land \frac{1}{T} \in ℂ) \to (x \in ℝ^{+} ⟼ \frac{1}{T}) \in 𝑂 (1)$
42	40 37 41	sylancr	$⊢ φ \to (x \in ℝ^{+} ⟼ \frac{1}{T}) \in 𝑂 (1)$
43	30 38 39 42	o1mul2	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n}) T (\frac{1}{T})) \in 𝑂 (1)$
44	36 43	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{μ (n)}{n})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrmusumlem

Proof