infinite sums of functions

Stream: Is there code for X?

[Floris van Doorn]

Do we already have lemmas about infinite sums of functions?

import topology.algebra.infinite_sum

lemma pi.has_sum {ι α β : Type*} [add_comm_monoid β] [topological_space β]
  {f : ι → α → β} {g : α → β} : has_sum f g ↔ ∀ x, has_sum (λ i, f i x) (g x) :=
sorry

If not, are there lemmas about tendsto for sequences functions?

[Floris van Doorn]

(I guess I can generalize α → β to ∀ x : α, β x)

[Patrick Massot]

What kind of lemma do you want?

[Heather Macbeth]

You have the product topology on α copies of β, and presumably also an add_comm_monoid structure on it. Can you interpret f as a map from ι to this add_comm_monoid + topological_space?

[Heather Macbeth]

Oh, I see, that's what you're doing.

[Floris van Doorn]

The lemma I want is

lemma measurable.ennreal_tsum {ι α} [measurable_space α]
  {f : ι → α → ennreal} (h : ∀ i, measurable (f i)) : measurable (∑' i, f i)

For this it is probably useful to know what the conclusion evaluates to (I could write measurable (λ x, ∑' i, f i x), but that seems less canonical)

[Floris van Doorn]

The sublemma I want is the lemma I posted in the first post.

[Patrick Massot]

I'm sorry I was distracted.

[Patrick Massot]

lemma pi.has_sum {ι α β : Type*} [add_comm_monoid β] [topological_space β]
  {f : ι → α → β} {g : α → β} : has_sum f g ↔ ∀ x, has_sum (λ i, f i x) (g x) :=
begin
  simp_rw [has_sum, nhds_pi, tendsto_infi, tendsto_comap_iff],
  apply forall_congr,
  intro a,
  convert iff.rfl,
  ext s,
  simp
end

[Floris van Doorn]

Thanks!