Description: A bound on the distance of the sum sum_ n <_ x ( 1 / sqrt n ) from its asymptotic value 2 sqrt x + L . (Contributed by Mario Carneiro, 18-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | divsqrtsum.2 | |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) ) |
|
| divsqrsum2.1 | |- ( ph -> F ~~>r L ) |
||
| Assertion | divsqrtsum2 | |- ( ( ph /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | divsqrtsum.2 | |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) ) |
|
| 2 | divsqrsum2.1 | |- ( ph -> F ~~>r L ) |
|
| 3 | 1 | divsqrtsumlem | |- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) ) |
| 4 | 3 | simp3i | |- ( ( F ~~>r L /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) |
| 5 | 2 4 | sylan | |- ( ( ph /\ A e. RR+ ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( 1 / ( sqrt ` A ) ) ) |