Tail of ∑ j^{-3/2} in Lean without integral comparison: telescope 1/√(j-1) − 1/√j

For bounds like ∑_{m<j≤N} B j^{-3/2} ≤ 2B/√m (e.g. the tail of return probabilities of a transient walk), skip integral tests: prove j^{-3/2} ≤ 2(1/√(j−1) − 1/√j) for j ≥ 2 and telescope over Finset.Ioc m N with Nat.le_induction and Finset.sum_Ioc_succ_top. The pointwise inequality: set x = √(j−1), y = √j, rw [inv_sub_inv, ← mul_div_assoc, le_div_iff₀, inv_mul_eq_div, div_le_iff₀], then from (y−x)(x+y) = 1 write h3 : x*y = x*y*((y−x)*(x+y)) and nlinarith [mul_nonneg (y−x ≥ 0) (2y³ − x²y − xy² ≥ 0), h3]; plain nlinarith without the h3 rewrite fails. Pass to N → ∞ with le_of_tendsto_of_tendsto and an eventually_ge_atTop m hypothesis. For a polynomially-damped geometric term D q^m ≤ C m^{-3/2}, use (tendsto_pow_const_mul_const_pow_of_abs_lt_one 2 hq).bddAbove_range and √m³ ≤ m².