Summable iff partial sums bounded

Stream: Is there code for X?

[Vincent Beffara]

Do we have this?

lemma summable_iff_bounded {u : ℕ → ℝ} (hu : 0 ≤ u) :
    Summable u ↔ BoundedAtFilter atTop (fun n => ∑ i in Finset.range n, u i) := by

summable_of_sum_range_le is close to one direction but it wants forall instead of eventually

[Kevin Buzzard]

I asked Github Copilot and it suggested starting with rw [summable_iff_cauchy_seq_finset] (which doesn't exist), so if you can guess what it's supposed to say then it might be missing API.

[Vincent Beffara]

def cumsum {E : Type*} [AddCommMonoid E] (u : ℕ → E) (n : ℕ) : E := ∑ i in Finset.range n, u i

lemma summable_iff_bounded {u : ℕ → ℝ} (hu : 0 ≤ u) : Summable u ↔ BoundedAtFilter atTop (cumsum u) := by

  have l0 : (cumsum u =O[atTop] 1) ↔ _ := isBigO_one_nat_atTop_iff (f := cumsum u)
  have l1 : Monotone (cumsum u) :=
    fun n₁ n₂ h₁₂ => Finset.sum_le_sum_of_subset_of_nonneg (by simp [h₁₂]) (fun i _ _ => hu i)
  have l2 i : |u i| = u i := abs_eq_self.mpr (hu i)
  have l4 n : 0 ≤ cumsum u n := Finset.sum_nonneg (fun i _ => hu i)
  have l3 n : ‖cumsum u n‖ = cumsum u n := by simp [Real.norm_eq_abs, abs_eq_self, l4]

  simp only [BoundedAtFilter, l0, l3]
  constructor <;> intro ⟨C, h1⟩
  · exact ⟨C, fun n => sum_le_hasSum _ (fun i _ => hu i) h1⟩
  · cases' tendsto_of_monotone l1 with h h
    · obtain ⟨n₀, h⟩ := tendsto_atTop_atTop.mp h (C + 1)
      linarith [h1 n₀, h n₀ le_rfl]
    · apply summable_of_absolute_convergence_real
      simpa only [l2]

[Jireh Loreaux]

How about docs#summable_of_norm_bounded or docs#summable_of_sum_le ?

[Jireh Loreaux]

Or if you really want partial sums docs#Real.tsum_le_of_sum_range_le

[Vincent Beffara]

I hadn't found that one, thanks!

lemma summable_iff_bounded {u : ℕ → ℝ} (hu : 0 ≤ u) : Summable u ↔ BoundedAtFilter atTop (cumsum u) := by

  have l0 : (cumsum u =O[atTop] 1) ↔ _ := isBigO_one_nat_atTop_iff (f := cumsum u)
  have l4 n : 0 ≤ cumsum u n := Finset.sum_nonneg (fun i _ => hu i)
  have l3 n : ‖cumsum u n‖ = cumsum u n := by simp [Real.norm_eq_abs, abs_eq_self, l4]

  simp only [BoundedAtFilter, l0, l3]
  constructor <;> intro ⟨C, h1⟩
  · exact ⟨C, fun n => sum_le_hasSum _ (fun i _ => hu i) h1⟩
  · exact summable_of_sum_range_le hu h1

Probably still golfable using incantations like lift u to N -> NNReal using hu or something, but that's for later.