Type alias for functions with uniform convergence topology

Stream: general

[Anatole Dedecker]

When I introduced docs#uniform_convergence.topological_space and all the related things a while ago, I had to decide wether I should just make them non-instance constructions on X -> Y or make them instances on a type synonym. For the reasons mentionned below, I chose not to make a type alias, but this question came up in basically all of the PR reviews related to this and after working with my definitions my opinion is not clear anymore, so I figured it would be nice to discuss it properly.

So, basically, my main point for not introducing a type alias was that, in most of the use case I have in mind, we only use this topology on a more specific hom type, not just bare functions (typically, continuous linear maps or bounded continuous maps), which suggests that it may not help at all to make them instances (except for developping the basic theory, but we can have local instances).
Another reason I was reluctant to make a type alias is that I'm never quite sure how to make them work properly, especially for function types. Typically, I remember having troubles when using docs#weak_dual, because type ascriptions between defeq types are sometimes completely ignored, which means that in some cases one has to use @s anyway, and I fear this would be annoying here too.
Also, this is a minor concern, but if we want to make a type alias for docs#uniform_convergence.topology, then we almost surely want one for docs#uniform_convergence_on.topology, which means a lot of boilerplate.

On the other hand, #16467 is a clear case where we do use uniform convergence on bare functions: one key fact about equicontinuity is that a family 𝓕 : ι → X → α is equicontinuous at iff the function swap 𝓕 : X → ι → α is continuous at when ι → α is equipped with the topology of uniform convergence. And, although I wrote in the docstring of this lemma that it should only be used for API building, there are a lot of places where it is really useful to factor code (see for example the topology/algebra/equicontinuity file introduced in #17128).

So at that point, I'm not sure what to do anymore. Basically the question is "is it worth investing in the boilerplate required by the type-alias approach, or will this be used rarely enough that having something slightly painful is fine ?", and I'd like to get some opinion on that before trying the type-alias approach.

cc @Patrick Massot @Sebastien Gouezel @Floris van Doorn @Moritz Doll @Jireh Loreaux

[Floris van Doorn]

Anatole Dedecker said:

type ascriptions between defeq types are sometimes completely ignored

Try to avoid type ascriptions to translate between defeq types. Instead use functions like docs#order_dual.to_dual and docs#order_dual.of_dual. You are allowed to abuse defeq, but only if the type of what you're doing is already known (e.g. docs#order_dual.forall). Although I realize that this might be annoying for function types... Maybe you only need the function to your type alias (e.g. to_uniform (swap 𝓕)) but you can make your eliminator (of_uniform) silent. I think this will be fine, since if f lives in your type alias, f x can still only mean one thing, and I expect you won't use any/much type-classes on the type X -> Y itself.

I would try the type alias if I were you.

[Anatole Dedecker]

Thanks for your input Floris!

[Sebastien Gouezel]

I would also try the type alias. Like Floris, I expect it should work pretty smoothly.

[Anatole Dedecker]

I've just opened #17516 which implements the type alias approach (I still need to adapt all the docstrings, but apart from that it is ready for review). I works quite smoothly indeed, although I find the "try adding of_funs until Lean infers what you want" part quite unsatisfying, but I think overall it is an improvement over what we currently have.

[Anatole Dedecker]

It should now be ready for review