Description: The sum sum_ n <_ x ( 1 / sqrt n ) is asymptotic to 2 sqrt x + L with a finite limit L . (In fact, this limit is zeta ( 1 / 2 ) ~-u 1 . 4 6 ... .) (Contributed by Mario Carneiro, 9-May-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | divsqrtsum.2 | |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) ) |
|
| Assertion | divsqrsum | |- F e. dom ~~>r |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | divsqrtsum.2 | |- F = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( 1 / ( sqrt ` n ) ) - ( 2 x. ( sqrt ` x ) ) ) ) |
|
| 2 | 1 | divsqrtsumlem | |- ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r 1 /\ 1 e. RR+ ) -> ( abs ` ( ( F ` 1 ) - 1 ) ) <_ ( 1 / ( sqrt ` 1 ) ) ) ) |
| 3 | 2 | simp2i | |- F e. dom ~~>r |