summable.single_le_tsum

Stream: Is there code for X?

[Damiano Testa]

Dear All,

in analogy with docs#finset.single_le_sum, I was looking for the similar statement for infinite sums, but could not find it. Is the lemma below (or something similar) in mathlib?

Thanks!

import topology.algebra.infinite_sum

namespace summable

variables {α β : Type*} [ordered_add_comm_group α] [topological_space α]
  [order_closed_topology α] [topological_add_group α] {f : β → α}

lemma single_le_tsum (a : β) (fs : summable f) (f0 : ∀ {x}, 0 ≤ f x) :
  f a ≤ ∑' x, f x :=
begin
  classical,
  refine (le_add_of_nonneg_right (tsum_nonneg (λ z, _))).trans (tsum_ite_eq_extract fs a).ge,
  split_ifs,
  exacts [rfl.le, f0]
end

end summable

[Sebastien Gouezel]

docs#le_tsum ?

[Damiano Testa]

looks like it's exactly what I need, thanks!

[Damiano Testa]

Indeed, this works! Thanks!

lemma single_le_tsum (a : β) (fs : summable f) (f0 : ∀ {x}, 0 ≤ f x) :
  f a ≤ ∑' x, f x :=
le_tsum fs a (λ s hs, f0)