Locally uniform convergence

Stream: maths

[David Loeffler]

What is the motivation for Mathlib's definition of "locally uniform convergence"?

If X is a top. space, Y a metric space, and $f_n$ a sequence of functions $X \to Y$, I would expect "$f_n$ converges locally uniformly to $g$" to mean that for every $x \in X$, there is a neighbourhood $U$ of $x$ upon which $f_n$ converges uniformly to $g$ -- i.e., the quantifiers go
"$\forall x \in X,\ \exists U \in \mathcal{N} x,\ \forall \epsilon > 0,\ \exists N,\, \forall n \ge N,\, \forall y \in U, d(f_n(y), f(y)) < \epsilon$".

But Mathlib's definition, docs#TendstoLocallyUniformly, is different: it has the quantifiers in a different order, so the condition is
"$\forall x \in X,\ \forall \epsilon > 0,\ \exists U \in \mathcal{N} x,\ \exists N,\, \forall n \ge N,\, \forall y \in U, d(f_n(y), f(y)) < \epsilon$".
So this version allows U to depend on $\epsilon$, while my version above requires that it be independent of $\epsilon$. Hence the second version is a priori weaker, although equivalent if $X$ is locally compact.

I'm pretty sure the definition I gave is the standard one for "locally uniform convergence", conforming to the general principle that "locally P" for absolutely any property of topological spaces means "each point has a neighbourhood such that P". I've not seen any sources which use Mathlib's interpretation. For instance, this paper https://www.jstage.jst.go.jp/article/pjab1945/36/3/36_3_102/_pdf/-char/en considers both notions, but uses the name "locally uniform convergence" for the first (stronger) condition above, and uses a different name ("uniform convergence at each point") for the second (weaker) condition.

(See also this MathOverflow question : https://mathoverflow.net/questions/187193/between-compact-and-locally-uniform-what-is-the-name-of-this-convergence, which again considers both topologies, but agrees with me about which should be called "locally uniform convergence")

So why is Mathlib using non-standard terminology here?

[David Loeffler]

(Tagging @Sébastien Gouëzel who is credited as the original author of the mathlib file in which this definition appears.)

[Sébastien Gouëzel]

To me, the second definition looks mathematically more useful, which is why I went for this one (without checking any reference): it is weaker than the first one (so easier to check), but sufficient for the main property I expect of locally uniform convergence, i.e., a locally uniform limit of continuous functions is continuous. If you have examples of theorems for which the right assumption is the first one, then we could definitely switch (or keep both with two different names).

[Antoine Chambert-Loir]

I tried to think (no more than 5 minutes, and without success) whether your second definition corresponds to a general topological/uniform structure. In general, it seems important that “locally something” really means that it is the local version of “something”. (And this could be automatized.)

[David Loeffler]

I think Sebastien makes a very persuasive point, that the weaker condition is sufficient for the main application (proving continuity of the limit). I don't have an example of a theorem that's substantially easier to prove with the other condition; my only concern, like Antoine, is the risk of surprise / puzzlement to users who naturally expect that "locally P" means "every point has a neighbourhood such that P".

Perhaps the way forward is to stick with the definition we currently have, but add a really clear and prominent explanation in the docs about the two versions and how they differ, and a lemma showing that the "$\exists U, \forall \epsilon$" version implies the "$\forall \epsilon, \exists U$" version (which we don't currently have, AFAIK, although we do have the equivalence of the two notions for locally-compact spaces).

[Kevin Buzzard]

You're not tempted to change the current definition to TendstoPointwiseUniformly or something, and add the natural proposed definition as well? Maybe this makes everyone happy? And you can have an explanation of the difference in both docstrings plus references from each to the other.

[David Loeffler]

Kevin's suggestion would certainly be option, but the lack of a good well-established name for this concept is a problem; calling it "TendstoPointwiseUniformly" might lead a lot of users to think "but isn't pointwise the opposite of uniformly?". Also, as Sebastian points out, there don't seem to be any natural examples of theorems for which the former hypothesis suffices but the latter doesn't.

[Kevin Buzzard]

OK then maybe "warning in docstring" is the way to go, at least for now.

[Antoine Chambert-Loir]

I don't agree. It can only bring more confusion at later stages. I believe “Locally…” should be this, and Sébastien's definition an easy theorem.

[David Loeffler]

@Antoine Chambert-Loir If we don't include Sebastien's definition as a definition, how would we formulate the theorem (already in Mathlib) that Sebastien's weaker definition is sufficient to imply that the limit $f$ is continuous if each $f_n$ is?

[Antoine Chambert-Loir]

I believe that Sébastien's definition should be included (eg as TendstoPointwiseUniformly), the initial theorem of Sébastien renamed using the new terminology, a new theorem defined saying that locally uniform convergence implies this property, and another one about preservation of continuity (possibly building on Sébastien's), as well as the equivalence between the two definitions when the space is locally compact. (Is it enough that its topology be compactly generated?)

[Antoine Chambert-Loir]

Now, this requires an hour or two of work, and I agree that it could be left to another day, by somebody else than you, and that for now a “TODO” and a warning in the docstringcould be enough.

[David Loeffler]

OK, I suggest the following. For now I will make a PR which splits the file UniformSpace/UniformConvergence.lean into 3 pieces, with one piece on locally uniform convergence, and make a clear explanation in the docstring of that file about how the two notions of locally-uniform convergence differ. Then Antoine, or anyone else, is welcome to return to this in future so we have both notions implemented and the relation between them; but I will not do it for now.

[Jireh Loreaux]

I agree that we should not add the usual definition until it becomes necessary. Note that the MathOverflow question you linked in the OP has an answer that makes a very persuasive argument that Mathlib's definition is really the a natural one.

[Antoine Chambert-Loir]

Simon Henry says that this notion of convergence “does not come from a topology”, and it is shown to be well behaved only on continuous functions, two points that I interpret as being an argument against the idea that this definition is natural.

[David Loeffler]

David Loeffler said:

OK, I suggest the following. For now I will make a PR which splits the file UniformSpace/UniformConvergence.lean into 3 pieces, with one piece on locally uniform convergence, and make a clear explanation in the docstring of that file about how the two notions of locally-uniform convergence differ.

PR up at #24342. (The only thing that is actually new in this PR is the module docstring of LocallyUniformConvergence.lean.)

[Anatole Dedecker]

Outside of Mathlib, the first time I encountered this notion is in "Champs continus d'espaces hilbertiens et de C*-algèbres" by Dixmier and Douady, where they indeed claim that this is not necessarily topologizable. In fact, even though they don't state it in these terms, the fourth axiom in their definition of "continuous field of Banach space" is that the space of continuous sections is closed under this weak notion of locally uniform limits (with the extra twist that they have dependent spaces of course).

[Anatole Dedecker]

I would argue that this notion (and the more general docs#TenstoUniformlyOnFilter) are definitely useful. As @Jireh Loreaux reminded me, we proved a version of Dini's theorem for this notion (docs#Monotone.tendstoLocallyUniformly_of_forall_tendsto), which I think isn't true for the stronger version.

[David Loeffler]

David Loeffler said:

OK, I suggest the following. For now I will make a PR which splits the file UniformSpace/UniformConvergence.lean into 3 pieces [...]

PR up at #24342. (The only thing that is actually new in this PR is the module docstring of LocallyUniformConvergence.lean.)

:ping_pong:

[Johan Commelin]

Thanks for the ping:

[David Loeffler]

Thanks Johan!