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.

[Andrew Yang]

Why does HasProdUniformlyOn take a family of sets instead of just one set?
Context: I am trying to restate docs#tendstoUniformlyOn_tsum and friends to HasProdUniformlyOn and I am wondering if we were happy with the following or if we want the set family version.

theorem summableUniformlyOn_tsum {f : α → β → F} (hu : Summable u) {s : Set β}
    (hfu : ∀ n x, x ∈ s → ‖f n x‖ ≤ u n) : SummableUniformlyOn f {s}

I am guessing we should just make SummableUniformlyOn take only one set but I have little experience around these.

[Chris Birkbeck]

IIRC it was todo with being able to match or use what we have for UniformOnFun which takes a family of sets.

[Andrew Yang]

It is hard to recover β →ᵤ[𝔖] F from β →ᵤ[{s}] F but it is easy to recover SummableUniformlyOn f 𝔖 from SummableUniformlyOn f {s} via ∀ s ∈ 𝔖, SummableUniformlyOn f {s}. So I think it is reasonable to stick with SummableUniformlyOn f {s} (i.e. redefine SummableUniformlyOn to take a set instead of a bunch of sets) so that the *On predicates have a more uniform API?

[Chris Birkbeck]

I sort of agree, so far I've only used if for a single set. But maybe @David Loeffler has some thoughts on this?

[David Loeffler]

Is it actually true that SummableUniformlyOn f 𝔖 is equivalent to ∀ s ∈ 𝔖, SummableUniformlyOn f {s}? It is true for HasSum, but for the Summable statement we might have some horrible situation where the sum over each s was convergent but the limit depended on which s you took. Probably this is impossible if the target space is Hausdorff but it's not "definitionally impossible".

[Andrew Yang]

Good point. I agree my claim above is not always true. But do we need this extra bit of flexibility?

[Andrew Yang]

Here is the PR attempting the change: #31293

[David Loeffler]

I think the extra bit of flexibility (coming from the difference between∀ s ∈ 𝔖, ∃ g, ... vs ∃ g, ∀ s∈ 𝔖, ...) is not that useful, because the two conditions are equivalent when the target space is T2, and without this sanity assumption the theory of infinite sums / products is a mess anyway. I think it's a good idea to get rid of the set families.

[Aaron Liu]

David Loeffler said:

Is it actually true that SummableUniformlyOn f 𝔖 is equivalent to ∀ s ∈ 𝔖, SummableUniformlyOn f {s}? It is true for HasSum, but for the Summable statement we might have some horrible situation where the sum over each s was convergent but the limit depended on which s you took. Probably this is impossible if the target space is Hausdorff but it's not "definitionally impossible".

Uniform spaces are pretty nice, they are R1-separated, meaning if you quotient out by the equivalence relation of "topologically indistinguishable" (pass to the docs#SeparationQuotient) you get a hausdorff space

[Aaron Liu]

And for a set of topologically indistinguishable points, if you converge to one you converge to all, so that shouldn't affect summability.

[David Loeffler]

@Aaron Liu Interesting. Are you saying you can deduce SummableUniformlyOn f 𝔖 from ∀ s ∈ 𝔖, SummableUniformlyOn f {s} without assuming the target of f is Hausdorff (or T0, which is equivalent in this setting)?

[Aaron Liu]

I'm saying, it shouldn't be a problem to assume all your spaces are hausdorff (since they basically are)

[David Loeffler]

I do not understand what you mean, since it is definitely not the case that a uniform space is automatically Hausdorff.

[Aaron Liu]

But a T0 uniform space is hausdorff, and all spaces are essentially T0

[David Loeffler]

You are using words like "basically" and "essentially" in ways that I am struggling to attach a rigorous meaning to.

[Aaron Liu]

I was using "basically" in an informal manner

[Aaron Liu]

"all spaces are essentially T0" means that every space is equivalent to a T0 space

[David Loeffler]

Where "equivalent" means what, may I ask?

[Andrew Yang]

I think what Aaron is trying to say is yes to the following

David Loeffler said:

Aaron Liu Interesting. Are you saying you can deduce SummableUniformlyOn f 𝔖 from ∀ s ∈ 𝔖, SummableUniformlyOn f {s} without assuming the target of f is Hausdorff (or T0, which is equivalent in this setting)?

Because you can do this on the t0 quotient (i.e. quotient by the inseparable relation), and any lift would still be a limit.

[David Loeffler]

I think that's what he's trying to say as well, but it's not self-explanatory to me that this works.

[Aaron Liu]

David Loeffler said:

Where "equivalent" means what, may I ask?

Continuous function with continuous not-quite-inverse such that both ways composition is pointwise inseparable from identity function

[David Loeffler]

This is not what "topological equivalence" means in mathlib (where it's a synonym for "homeomorphism").

To explain a little more what I was getting at above: if X, Y are uniform spaces, then functions X -> Y are a uniform space in a natural way (this is UniformOnFun in mathlib). With this uniform structure, is the separation quotient of X --> Y the same as X --> (separation quotient of Y)? It seems plausible, but not entirely self-evident; and I think this what's needed to make the argument work.

(EDIT: I mean uniformly-continuous functions here, not arbitrary functions, sorry.)

[Aaron Liu]

yes it is

[Aaron Liu]

obviously

[Aaron Liu]

maybe not that obvious

[Aaron Liu]

well, it should at least be true that sepquot(X->Y) is uniform isomorphic to sepquot(X->sepquot(Y))

[David Loeffler]

@Aaron Liu If you feel like a challenge, perhaps you might like to try proving SummableUniformlyOn.hasSumUniformlyOn (maybe just for 𝔖 = {s} a singleton) with the [T2Space α] hypothesis removed. (Note that there is no such hypothesis in Summable.hasSum.)

[Aaron Liu]

David Loeffler said:

Aaron Liu If you feel like a challenge, perhaps you might like to try proving SummableUniformlyOn.hasSumUniformlyOn (maybe just for 𝔖 = {s} a singleton) with the [T2Space α] hypothesis removed. (Note that there is no such hypothesis in Summable.hasSum.)

#31313

[Yongxi Lin (Aaron)]

A related PR #31377