SummableUniformlyOn

Stream: mathlib4

[Chris Birkbeck]

As part of #13349 one suggestion I've had from @David Loeffler is to maybe define the notion of summableUniformlyOn (and multipliable versions), for infinite sums/products that converge uniformly on some subset. I guess we could start with something like:

def HasProdUniformlyOn (f : ι → β → α) (g : β → α) (s : Set β) : Prop :=
  TendstoUniformlyOn (fun (s : Finset ι) b ↦ ∏ i ∈ s, f i b) g atTop s

and then build the API from there. Are there any thoughts/suggestions on this approach?

[Andrew Yang]

I have no idea how to do it properly but I agree we should definitely have some form of this.