dchrisum

Description: If n e. [ M , +oo ) |-> A ( n ) is a positive decreasing function approaching zero, then the infinite sum sum_ n , X ( n ) A ( n ) is convergent, with the partial sum sum_ n <_ x , X ( n ) A ( n ) within O ( A ( M ) ) of the limit T . Lemma 9.4.1 of Shapiro, p. 377. (Contributed by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	rpvmasum.z	$⊢ Z = ℤ / N ℤ$
	rpvmasum.l	$⊢ L = ℤRHom (Z)$
	rpvmasum.a	$⊢ φ \to N \in ℕ$
	rpvmasum.g	$⊢ G = DChr (N)$
	rpvmasum.d	$⊢ D = {Base}_{G}$
	rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
	dchrisum.b	$⊢ φ \to X \in D$
	dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
	dchrisum.2	$⊢ n = x \to A = B$
	dchrisum.3	$⊢ φ \to M \in ℕ$
	dchrisum.4	$⊢ (φ \land n \in ℝ^{+}) \to A \in ℝ$
	dchrisum.5	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
	dchrisum.6	$⊢ φ \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
	dchrisum.7	$⊢ F = (n \in ℕ ⟼ X (L (n)) A)$
Assertion	dchrisum	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B)$

Proof

Step	Hyp	Ref	Expression
1		rpvmasum.z	$⊢ Z = ℤ / N ℤ$
2		rpvmasum.l	$⊢ L = ℤRHom (Z)$
3		rpvmasum.a	$⊢ φ \to N \in ℕ$
4		rpvmasum.g	$⊢ G = DChr (N)$
5		rpvmasum.d	$⊢ D = {Base}_{G}$
6		rpvmasum.1	$⊢ \underset{˙}{1} = 0_{G}$
7		dchrisum.b	$⊢ φ \to X \in D$
8		dchrisum.n1	$⊢ φ \to X \neq \underset{˙}{1}$
9		dchrisum.2	$⊢ n = x \to A = B$
10		dchrisum.3	$⊢ φ \to M \in ℕ$
11		dchrisum.4	$⊢ (φ \land n \in ℝ^{+}) \to A \in ℝ$
12		dchrisum.5	$⊢ (φ \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
13		dchrisum.6	$⊢ φ \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
14		dchrisum.7	$⊢ F = (n \in ℕ ⟼ X (L (n)) A)$
15		fzofi	$⊢ (0 ..^N) \in Fin$
16		fzofi	$⊢ (0 ..^u) \in Fin$
17	16	a1i	$⊢ φ \to (0 ..^u) \in Fin$
18	7	adantr	$⊢ (φ \land m \in (0 ..^u)) \to X \in D$
19		elfzoelz	$⊢ m \in (0 ..^u) \to m \in ℤ$
20	19	adantl	$⊢ (φ \land m \in (0 ..^u)) \to m \in ℤ$
21	4 1 5 2 18 20	dchrzrhcl	$⊢ (φ \land m \in (0 ..^u)) \to X (L (m)) \in ℂ$
22	17 21	fsumcl	$⊢ φ \to \sum_{m \in (0 ..^u)} X (L (m)) \in ℂ$
23	22	abscld	$⊢ φ \to \|\sum_{m \in (0 ..^u)} X (L (m))\| \in ℝ$
24	23	ralrimivw	$⊢ φ \to \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \in ℝ$
25		fimaxre3	$⊢ ((0 ..^N) \in Fin \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \in ℝ) \to \exists r \in ℝ \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r$
26	15 24 25	sylancr	$⊢ φ \to \exists r \in ℝ \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r$
27	3	adantr	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to N \in ℕ$
28	7	adantr	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to X \in D$
29	8	adantr	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to X \neq \underset{˙}{1}$
30	10	adantr	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to M \in ℕ$
31	11	adantlr	$⊢ ((φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \land n \in ℝ^{+}) \to A \in ℝ$
32	12	3adant1r	$⊢ ((φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \land (n \in ℝ^{+} \land x \in ℝ^{+}) \land (M \leq n \land n \leq x)) \to B \leq A$
33	13	adantr	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to (n \in ℝ^{+} ⟼ A) \underset{ℝ}{⇝} 0$
34		simprl	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to r \in ℝ$
35		simprr	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r$
36		2fveq3	$⊢ m = n \to X (L (m)) = X (L (n))$
37	36	cbvsumv	$⊢ \sum_{m \in (0 ..^u)} X (L (m)) = \sum_{n \in (0 ..^u)} X (L (n))$
38		oveq2	$⊢ u = i \to (0 ..^u) = (0 ..^i)$
39	38	sumeq1d	$⊢ u = i \to \sum_{n \in (0 ..^u)} X (L (n)) = \sum_{n \in (0 ..^i)} X (L (n))$
40	37 39	eqtrid	$⊢ u = i \to \sum_{m \in (0 ..^u)} X (L (m)) = \sum_{n \in (0 ..^i)} X (L (n))$
41	40	fveq2d	$⊢ u = i \to \|\sum_{m \in (0 ..^u)} X (L (m))\| = \|\sum_{n \in (0 ..^i)} X (L (n))\|$
42	41	breq1d	$⊢ u = i \to (\|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r \leftrightarrow \|\sum_{n \in (0 ..^i)} X (L (n))\| \leq r)$
43	42	cbvralvw	$⊢ \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r \leftrightarrow \forall i \in (0 ..^N) \|\sum_{n \in (0 ..^i)} X (L (n))\| \leq r$
44	35 43	sylib	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to \forall i \in (0 ..^N) \|\sum_{n \in (0 ..^i)} X (L (n))\| \leq r$
45	1 2 27 4 5 6 28 29 9 30 31 32 33 14 34 44	dchrisumlem3	$⊢ (φ \land (r \in ℝ \land \forall u \in (0 ..^N) \|\sum_{m \in (0 ..^u)} X (L (m))\| \leq r)) \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B)$
46	26 45	rexlimddv	$⊢ φ \to \exists t \exists c \in [0, +∞) (seq 1 (+ F) ⇝ t \land \forall x \in [M, +∞) \|seq 1 (+ F) (⌊x⌋) - t\| \leq c B)$

Metamath Proof Explorer

Theorem dchrisum

Proof