feat(Analysis/PSeries): some summability results (#11150)

Summability of `n ↦ 1 / |n + a| ^ s` and `n ↦ n ^ k exp (-r * n)`

Mathlib/Analysis/PSeries.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury G. Kudryashov
 -/
 import Mathlib.Analysis.SpecialFunctions.Pow.NNReal
+import Mathlib.Analysis.SpecialFunctions.Pow.Continuity
 import Mathlib.Analysis.SumOverResidueClass
 
 #align_import analysis.p_series from "leanprover-community/mathlib"@"0b9eaaa7686280fad8cce467f5c3c57ee6ce77f8"
@@ -354,3 +355,42 @@ lemma Real.not_summable_indicator_one_div_natCast {m : ℕ} (hm : m ≠ 0) (k :
   simp_rw [indicator_apply, mem_setOf, cast_add, cast_one, ← eq_sub_iff_add_eq, ← h]
   rw [summable_indicator_mod_iff (fun n₁ n₂ h ↦ by gcongr) (k - 1)]
   exact mt (summable_nat_add_iff (f := fun n : ℕ ↦ 1 / (n : ℝ)) 1).mp not_summable_one_div_nat_cast
+
+/-!
+## Translating the `p`-series by a real number
+-/
+section shifted
+
+open Filter Asymptotics Topology
+
+lemma Real.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_nat_cast_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
+      field_simp [(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]
+
+lemma Real.summable_one_div_int_add_rpow (a : ℝ) (s : ℝ) :
+    Summable (fun n : ℤ ↦ 1 / |n + a| ^ s) ↔ 1 < s := by
+  simp_rw [summable_int_iff_summable_nat_and_neg, ← abs_neg (↑(-_ : ℤ) + a), neg_add,
+    Int.cast_neg, neg_neg, Int.cast_ofNat, summable_one_div_nat_add_rpow, and_self]
+
+end shifted

Mathlib/Analysis/SpecialFunctions/Exp.lean

@@ -433,6 +433,12 @@ lemma summable_exp_nat_mul_iff {a : ℝ} :
 lemma summable_exp_neg_nat : Summable fun n : ℕ ↦ exp (-n) := by
   simpa only [mul_neg_one] using summable_exp_nat_mul_iff.mpr neg_one_lt_zero
 
+lemma summable_pow_mul_exp_neg_nat_mul (k : ℕ) {r : ℝ} (hr : 0 < r) :
+    Summable fun n : ℕ ↦ n ^ k * exp (-r * n) := by
+  simp_rw [mul_comm (-r), exp_nat_mul]
+  apply summable_pow_mul_geometric_of_norm_lt_one
+  rwa [norm_of_nonneg (exp_nonneg _), exp_lt_one_iff, neg_lt_zero]
+
 end Real
 
 namespace Complex