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 | ⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) | |
| divsqrsum2.1 | ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 ) | ||
| Assertion | divsqrtsum2 | ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | divsqrtsum.2 | ⊢ 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / ( √ ‘ 𝑛 ) ) − ( 2 · ( √ ‘ 𝑥 ) ) ) ) | |
| 2 | divsqrsum2.1 | ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 ) | |
| 3 | 1 | divsqrtsumlem | ⊢ ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) ) |
| 4 | 3 | simp3i | ⊢ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) |
| 5 | 2 4 | sylan | ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( 1 / ( √ ‘ 𝐴 ) ) ) |