## Stream: Is there code for X?

### Topic: infinite sums of functions

#### Floris van Doorn (Aug 25 2020 at 19:18):

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 (Aug 25 2020 at 19:19):

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

#### Patrick Massot (Aug 25 2020 at 19:41):

What kind of lemma do you want?

#### Heather Macbeth (Aug 25 2020 at 19:47):

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 (Aug 25 2020 at 19:48):

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

#### Floris van Doorn (Aug 25 2020 at 19:58):

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 (Aug 25 2020 at 20:00):

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

#### Patrick Massot (Aug 25 2020 at 20:47):

I'm sorry I was distracted.

#### Patrick Massot (Aug 25 2020 at 20:47):

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 (Aug 25 2020 at 20:48):

Thanks!

Last updated: May 07 2021 at 22:14 UTC