dchrvmasumlem

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	dchrvmasumlem	$⊢ φ \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	1 2 3 4 5 6 7 8 9 10 11 12	dchrisumn0	$⊢ φ \to T \neq 0$
14	13	adantr	$⊢ (φ \land x \in ℝ^{+}) \to T \neq 0$
15		ifnefalse	$⊢ T \neq 0 \to if (T = 0, \log x, 0) = 0$
16	14 15	syl	$⊢ (φ \land x \in ℝ^{+}) \to if (T = 0, \log x, 0) = 0$
17	16	oveq2d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (T = 0, \log x, 0) = \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + 0$
18		fzfid	$⊢ (φ \land x \in ℝ^{+}) \to (1 \dots ⌊x⌋) \in Fin$
19	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X \in D$
20		elfzelz	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℤ$
21	20	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℤ$
22	4 1 5 2 19 21	dchrzrhcl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X (L (n)) \in ℂ$
23		elfznn	$⊢ n \in (1 \dots ⌊x⌋) \to n \in ℕ$
24	23	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to n \in ℕ$
25		vmacl	$⊢ n \in ℕ \to Λ (n) \in ℝ$
26		nndivre	$⊢ (Λ (n) \in ℝ \land n \in ℕ) \to \frac{Λ (n)}{n} \in ℝ$
27	25 26	mpancom	$⊢ n \in ℕ \to \frac{Λ (n)}{n} \in ℝ$
28	24 27	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℝ$
29	28	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to \frac{Λ (n)}{n} \in ℂ$
30	22 29	mulcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in (1 \dots ⌊x⌋)) \to X (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
31	18 30	fsumcl	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) \in ℂ$
32	31	addid1d	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + 0 = \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n})$
33	17 32	eqtrd	$⊢ (φ \land x \in ℝ^{+}) \to \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (T = 0, \log x, 0) = \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n})$
34	33	mpteq2dva	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (T = 0, \log x, 0)) = (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}))$
35	1 2 3 4 5 6 7 8 9 10 11 12	dchrvmasumif	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n}) + if (T = 0, \log x, 0)) \in 𝑂 (1)$
36	34 35	eqeltrrd	$⊢ φ \to (x \in ℝ^{+} ⟼ \sum_{n = 1}^{⌊x⌋} X (L (n)) (\frac{Λ (n)}{n})) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem dchrvmasumlem

Proof