feat(analysis/specific_limits): basic ratio test for summability of a nat-indexed family (#7277)

Author: ADedecker

src/analysis/specific_limits.lean

@@ -199,6 +199,19 @@ lemma geom_le {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ k <
   c ^ n * u 0 ≤ u n :=
 by refine (monotone_mul_left_of_nonneg hc).seq_le_seq n _ _ h; simp [pow_succ, mul_assoc, le_refl]
 
+lemma lt_geom {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) {n : ℕ} (hn : 0 < n)
+  (h : ∀ k < n, u (k + 1) < c * u k) :
+  u n < c ^ n * u 0 :=
+begin
+  refine (monotone_mul_left_of_nonneg hc).seq_pos_lt_seq_of_lt_of_le hn _ h _,
+  { simp },
+  { simp [pow_succ, mul_assoc, le_refl] }
+end
+
+lemma le_geom {u : ℕ → ℝ} {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (h : ∀ k < n, u (k + 1) ≤ c * u k) :
+  u n ≤ (c ^ n) * u 0 :=
+by refine (monotone_mul_left_of_nonneg hc).seq_le_seq n _ h _; simp [pow_succ, mul_assoc, le_refl]
+
 /-- For any natural `k` and a real `r > 1` we have `n ^ k = o(r ^ n)` as `n → ∞`. -/
 lemma is_o_pow_const_const_pow_of_one_lt {R : Type*} [normed_ring R] (k : ℕ) {r : ℝ} (hr : 1 < r) :
   is_o (λ n, n ^ k : ℕ → R) (λ n, r ^ n) at_top :=
@@ -695,6 +708,82 @@ end
 
 end normed_ring_geometric
 
+/-! ### Summability tests based on comparison with geometric series -/
+
+lemma summable_of_ratio_norm_eventually_le {α : Type*} [semi_normed_group α] [complete_space α]
+  {f : ℕ → α} {r : ℝ} (hr₁ : r < 1)
+  (h : ∀ᶠ n in at_top, ∥f (n+1)∥ ≤ r * ∥f n∥) : summable f :=
+begin
+  by_cases hr₀ : 0 ≤ r,
+  { rw eventually_at_top at h,
+    rcases h with ⟨N, hN⟩,
+    rw ← @summable_nat_add_iff α _ _ _ _ N,
+    refine summable_of_norm_bounded (λ n, ∥f N∥ * r^n)
+      (summable.mul_left _ $ summable_geometric_of_lt_1 hr₀ hr₁) (λ n, _),
+    conv_rhs {rw [mul_comm, ← zero_add N]},
+    refine le_geom hr₀ n (λ i _, _),
+    convert hN (i + N) (N.le_add_left i) using 3,
+    ac_refl },
+  { push_neg at hr₀,
+    refine summable_of_norm_bounded_eventually 0 summable_zero _,
+    rw nat.cofinite_eq_at_top,
+    filter_upwards [h],
+    intros n hn,
+    by_contra h,
+    push_neg at h,
+    exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn $ mul_neg_of_neg_of_pos hr₀ h) }
+end
+
+lemma summable_of_ratio_test_tendsto_lt_one {α : Type*} [normed_group α] [complete_space α]
+  {f : ℕ → α} {l : ℝ} (hl₁ : l < 1) (hf : ∀ᶠ n in at_top, f n ≠ 0)
+  (h : tendsto (λ n, ∥f (n+1)∥/∥f n∥) at_top (𝓝 l)) : summable f :=
+begin
+  rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩,
+  refine summable_of_ratio_norm_eventually_le hr₁ _,
+  filter_upwards [eventually_le_of_tendsto_lt hr₀ h, hf],
+  intros n h₀ h₁,
+  rwa ← div_le_iff (norm_pos_iff.mpr h₁)
+end
+
+lemma not_summable_of_ratio_norm_eventually_ge {α : Type*} [semi_normed_group α]
+  {f : ℕ → α} {r : ℝ} (hr : 1 < r) (hf : ∃ᶠ n in at_top, ∥f n∥ ≠ 0)
+  (h : ∀ᶠ n in at_top, r * ∥f n∥ ≤ ∥f (n+1)∥) : ¬ summable f :=
+begin
+  rw eventually_at_top at h,
+  rcases h with ⟨N₀, hN₀⟩,
+  rw frequently_at_top at hf,
+  rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩,
+  rw ← @summable_nat_add_iff α _ _ _ _ N,
+  refine mt summable.tendsto_at_top_zero
+    (λ h', not_tendsto_at_top_of_tendsto_nhds (tendsto_norm_zero.comp h') _),
+  convert tendsto_at_top_of_geom_le _ hr _,
+  { refine lt_of_le_of_ne (norm_nonneg _) _,
+    intro h'',
+    specialize hN₀ N hNN₀,
+    simp only [comp_app, zero_add] at h'',
+    exact hN h''.symm },
+  { intro i,
+    dsimp only [comp_app],
+    convert (hN₀ (i + N) (hNN₀.trans (N.le_add_left i))) using 3,
+    ac_refl }
+end
+
+lemma not_summable_of_ratio_test_tendsto_gt_one {α : Type*} [semi_normed_group α]
+  {f : ℕ → α} {l : ℝ} (hl : 1 < l)
+  (h : tendsto (λ n, ∥f (n+1)∥/∥f n∥) at_top (𝓝 l)) : ¬ summable f :=
+begin
+  have key : ∀ᶠ n in at_top, ∥f n∥ ≠ 0,
+  { filter_upwards [eventually_ge_of_tendsto_gt hl h],
+    intros n hn hc,
+    rw [hc, div_zero] at hn,
+    linarith },
+  rcases exists_between hl with ⟨r, hr₀, hr₁⟩,
+  refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently _,
+  filter_upwards [eventually_ge_of_tendsto_gt hr₁ h, key],
+  intros n h₀ h₁,
+  rwa ← le_div_iff (lt_of_le_of_ne (norm_nonneg _) h₁.symm)
+end
+
 /-! ### Positive sequences with small sums on encodable types -/
 
 /-- For any positive `ε`, define on an encodable type a positive sequence with sum less than `ε` -/