limit of a sum over nat

Stream: Is there code for X?

[Kevin Buzzard]

I'm knocking up a quick implementation of binary expansions for LTE. I'm hoping that what we have about infinite sums already makes this easy but I don't immediately see how to do it cleanly (a version with reals instead of non-negative reals would also be fine):

import data.real.nnreal -- [0,∞)
import topology.algebra.infinite_sum -- infinite sums

open_locale nnreal -- notation ℝ≥0 for [0,∞)

open_locale big_operators -- notation ∑ for finite sums

open finset -- for finset.range

-- let a₀ a₁ a₂... be a sequence of non-negative reals and let r be a non-negative real
example (a : ℕ → ℝ≥0) (r : ℝ≥0)
  -- Suppose the finite sums of the aᵢ are bounded above by r
  (hle : ∀ B, ∑ n in range B, a n ≤ r)
  -- and get arbitrarily close to r.
  (hge : ∀ ε > 0, ∃ B, ε + ∑ n in range B, a n > r) :
  -- Then r is the sum.
has_sum a r :=
sorry

[Jireh Loreaux]

how about using docs#nnreal.has_sum_iff_tendsto_nat? There's still a bit of work involved, but I don't think it would be too bad.

[Jireh Loreaux]

There's also docs#has_sum_iff_tendsto_nat_of_nonneg for the real version with a nonnegativity hypothesis instead.

[Jireh Loreaux]

Another approach would be to go into ennreal directly, where you can use easy comparison results. For example, docs#ennreal.sum_le_tsum would allow you to use hge to get ε + ∑' n, (a n : ℝ≥0∞) > ↑r for all ε > 0, from which ∑' n, (a n : ℝ≥0∞) ≥ ↑r follows via docs#le_of_forall_pos_le_add. You could then use docs#nnreal.tsum_le_of_sum_range_le to get the other inequality (with some coercions), and then finally docs#nnreal.tsum_eq_to_nnreal_tsum to glue it back to nnreal.

[Kevin Buzzard]

ha ha it was using docs#summable.has_sum_iff_tendsto_nat which I think is essentially the same as nnreal.has_sum_iff_tendsto_nat, and then struggling a bit more, which was what prompted me to ask :-) Maybe you're right and ennreal is easier. Thanks!

[Jireh Loreaux]

I'm not sure ennreal is tons easier. I feel like we're probably missing a lemma here.

[Jireh Loreaux]

Also, someone probably knows the tsum library way better than me :laughing:

[Jireh Loreaux]

@Kevin Buzzard in case you want it, not golfed:

import data.real.nnreal -- [0,∞)
import topology.algebra.infinite_sum -- infinite sums
import topology.instances.ennreal

open_locale nnreal -- notation ℝ≥0 for [0,∞)

open_locale big_operators -- notation ∑ for finite sums

open finset -- for finset.range

-- let a₀ a₁ a₂... be a sequence of non-negative reals and let r be a non-negative real
example (a : ℕ → ℝ≥0) (r : ℝ≥0)
  -- Suppose the finite sums of the aᵢ are bounded above by r
  (hle : ∀ B, ∑ n in range B, a n ≤ r)
  -- and get arbitrarily close to r.
  (hge : ∀ ε > 0, ∃ B, ε + ∑ n in range B, a n > r) :
  -- Then r is the sum.
has_sum a r :=
begin
  rw nnreal.has_sum_iff_tendsto_nat,
  rw metric.tendsto_nhds,
  intros ε hε,
  lift ε to ℝ≥0 using hε.lt.le,
  rcases hge ε hε with ⟨B, hB⟩,
  rw filter.eventually_at_top,
  refine ⟨B, λ N hN, _⟩,
  rw nnreal.dist_eq,
  refine abs_lt.mpr ⟨_, _⟩,
  { rw [lt_sub_iff_add_lt', ←sub_eq_add_neg, sub_lt_iff_lt_add', (nat.add_sub_of_le hN).symm,
      finset.sum_range_add, nnreal.coe_add, ←add_assoc],
    exact lt_of_lt_of_le hB (le_add_of_nonneg_right nnreal.zero_le_coe), },
  { rw sub_lt_iff_lt_add,
    exact_mod_cast lt_of_le_of_lt (hle N) (lt_add_of_pos_left r hε), }
end

[Kevin Buzzard]

Thanks!

[Jireh Loreaux]

@Kevin Buzzard Here's the one via ℝ≥0∞. I think this is more the way a mathematician would think about it, and it's shorter. I was having trouble finding ennreal.tsum_eq_supr_sum before.

open_locale ennreal

example (a : ℕ → ℝ≥0) (r : ℝ≥0)
  -- Suppose the finite sums of the aᵢ are bounded above by r
  (hle : ∀ B, ∑ n in range B, a n ≤ r)
  -- and get arbitrarily close to r.
  (hge : ∀ ε > 0, ∃ B, ε + ∑ n in range B, a n > r) :
  -- Then r is the sum.
has_sum a r :=
begin
  rw ←ennreal.has_sum_coe, -- nnreal sums to an nnreal iff ennreal does
  convert ennreal.has_sum, -- ennreal has a sum which is the supremum over finite sums
  rw [←ennreal.tsum_eq_supr_sum, ennreal.tsum_eq_supr_nat], -- the supremum over finite sums is the supremum over all partial sums
  refine le_antisymm (ennreal.le_of_forall_pos_le_add (λ ε hε h, _))
    (supr_le (by exact_mod_cast hle)),
  obtain ⟨B, hB⟩ := hge ε hε,
  calc (r : ℝ≥0∞) ≤ ε + ∑ n in range B, (a n) : by exact_mod_cast ennreal.coe_mono hB.lt.le
  ...             ≤ _ : by { rw add_comm, exact add_le_add_right (le_supr _ B) _ }
end