boundedness of sums

Stream: Is there code for X?

[Kevin Buzzard]

Does the following follow from some general facts about sums?

lemma int.nat_bdd_of_summable (a : ℤ → ℝ) (ha : summable a) : ∃ B : ℝ,
  ∀ m, ∥∑' (n : ℕ), a (m + n)∥ ≤ B :=
begin
  sorry,
end

[Kevin Buzzard]

Oh I can just use ∑' (z : ℤ), ∥a z∥ for the bound and now it's straightforward (at least on paper). I was overthinking it.

[Kevin Buzzard]

lemma int.nat_bdd_of_summable (a : ℤ → ℝ) (ha : summable a) (m : ℤ) :
  ∥∑' (n : ℕ), a (m + n)∥ ≤ ∑' (z : ℤ), ∥a z∥ :=
begin
  have hinj : function.injective (λ (n : ℕ), m + n),
  { rintros a b (h : m + a = m + b),
    simpa using h },
  rw ← summable_norm_iff at ha,
  refine le_trans (norm_tsum_le_tsum_norm (ha.comp_injective hinj)) _,
  exact tsum_le_tsum_of_inj _ hinj (λ _ _, norm_nonneg _) (λ _, le_refl _)
    (ha.comp_injective hinj) ha,
end

[Floris van Doorn]

See also docs#add_right_injective