Zulip Chat Archive

Stream: Is there code for X?

Topic: infinite sums of functions


view this post on Zulip Floris van Doorn (Aug 25 2020 at 19:18):

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?

view this post on Zulip Floris van Doorn (Aug 25 2020 at 19:19):

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

view this post on Zulip Patrick Massot (Aug 25 2020 at 19:41):

What kind of lemma do you want?

view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Aug 25 2020 at 19:48):

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

view this post on Zulip 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)

view this post on Zulip Floris van Doorn (Aug 25 2020 at 20:00):

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

view this post on Zulip Patrick Massot (Aug 25 2020 at 20:47):

I'm sorry I was distracted.

view this post on Zulip 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

view this post on Zulip Floris van Doorn (Aug 25 2020 at 20:48):

Thanks!


Last updated: May 07 2021 at 22:14 UTC