English
For real a and s, the series ∑_{n≥1} 1/|n+a|^s converges if and only if s > 1.
Русский
Для вещественных a и s ряд ∑_{n≥1} 1/|n+a|^s сходится тогда и только тогда, когда s > 1.
LaTeX
$$$$\displaystyle \sum_{n=1}^{\infty} \frac{1}{|n+a|^{s}} < \infty \quad\text{iff}\quad s>1.$$$$
Lean4
theorem summable_one_div_nat_add_rpow (a : ℝ) (s : ℝ) : Summable (fun n : ℕ ↦ 1 / |n + a| ^ s) ↔ 1 < s :=
by
suffices ∀ (b c : ℝ), Summable (fun n : ℕ ↦ 1 / |n + b| ^ s) → Summable (fun n : ℕ ↦ 1 / |n + c| ^ s) by
simp_rw [← summable_one_div_nat_rpow, Iff.intro (this a 0) (this 0 a), add_zero, Nat.abs_cast]
refine fun b c h ↦ summable_of_isBigO_nat h (isBigO_of_div_tendsto_nhds ?_ 1 ?_)
· filter_upwards [eventually_gt_atTop (Nat.ceil |b|)] with n hn hx
have hna : 0 < n + b := by linarith [lt_of_abs_lt ((abs_neg b).symm ▸ Nat.lt_of_ceil_lt hn)]
exfalso
revert hx
positivity
· simp_rw [Pi.div_def, div_div, mul_one_div, one_div_div]
refine (?_ : Tendsto (fun x : ℝ ↦ |x + b| ^ s / |x + c| ^ s) atTop (𝓝 1)).comp tendsto_natCast_atTop_atTop
have : Tendsto (fun x : ℝ ↦ 1 + (b - c) / x) atTop (𝓝 1) := by
simpa using tendsto_const_nhds.add ((tendsto_const_nhds (X := ℝ)).div_atTop tendsto_id)
have : Tendsto (fun x ↦ (x + b) / (x + c)) atTop (𝓝 1) :=
by
refine (this.comp (tendsto_id.atTop_add (tendsto_const_nhds (x := c)))).congr' ?_
filter_upwards [eventually_gt_atTop (-c)] with x hx
simp [field, (by linarith : 0 < x + c).ne']
apply (one_rpow s ▸ (continuousAt_rpow_const _ s (by simp)).tendsto.comp this).congr'
filter_upwards [eventually_gt_atTop (-b), eventually_gt_atTop (-c)] with x hb hc
rw [neg_lt_iff_pos_add] at hb hc
rw [Function.comp_apply, div_rpow hb.le hc.le, abs_of_pos hb, abs_of_pos hc]
